The cat eats the lion. The cat is big. The cat is round. The cat needs the lion. The lion eats the cat. The lion is big. The lion is green. The lion is not nice. The lion is young. The lion sees the cat. If someone is nice then they do not see the cat. If someone is round and they see the lion then the lion is not green. If someone eats the cat and they are not big then they need the lion. If the cat sees the lion then the cat eats the lion. All round people are nice. If someone eats the lion and the lion is not big then the lion does not see the cat. If someone eats the lion and the lion needs the cat then they are not green. If the lion sees the cat then the lion eats the cat.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is not nice.
("lion" "is" "nice" "-")
The lion is young.
("lion" "is" "young" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
If someone is nice then they do not see the cat.
((("someone" "is" "nice" "+")) -> ("someone" "sees" "cat" "-"))
If someone is round and they see the lion then the lion is not green.
((("someone" "is" "round" "+") ("someone" "sees" "lion" "+")) -> ("lion" "is" "green" "-"))
If someone eats the cat and they are not big then they need the lion.
((("someone" "eats" "cat" "+") ("someone" "is" "big" "~")) -> ("someone" "needs" "lion" "+"))
If the cat sees the lion then the cat eats the lion.
((("cat" "sees" "lion" "+")) -> ("cat" "eats" "lion" "+"))
All round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone eats the lion and the lion is not big then the lion does not see the cat.
((("someone" "eats" "lion" "+") ("lion" "is" "big" "~")) -> ("lion" "sees" "cat" "-"))
If someone eats the lion and the lion needs the cat then they are not green.
((("someone" "eats" "lion" "+") ("lion" "needs" "cat" "+")) -> ("someone" "is" "green" "-"))
If the lion sees the cat then the lion eats the cat.
((("lion" "sees" "cat" "+")) -> ("lion" "eats" "cat" "+"))
The lion is not nice.
True
1
proof
[(triple8)]
("lion" "is" "nice" "-")
triple8
The cat is not round.
False
1
inv-proof
[(triple3)]
("cat" "is" "round" "-")
triple3
The cat is nice.
True
2
proof
[(((triple3) -> rule5))]
("cat" "is" "nice" "+")
((triple3) -> (rule5 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is not nice.
False
2
inv-proof
[(((triple3) -> rule5))]
("cat" "is" "nice" "-")
((triple3) -> (rule5 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat does not see the cat.
True
3
proof
[(((((triple3) -> rule5)) -> rule1))]
("cat" "sees" "cat" "-")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
The cat does not see the cat.
("cat" "sees" "cat" "-")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat sees the cat.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule1))]
("cat" "sees" "cat" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
The cat does not see the cat.
("cat" "sees" "cat" "-")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The lion does not need the lion.
Unknown
inv-rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "needs" "lion" "-")
The cat sees the lion.
Unknown
random
[@0: The cat sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "lion" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat eats the lion.[(triple1)] The cat is big.[(triple2)] The cat is round.[(triple3)] The cat needs the lion.[(triple4)] The lion eats the cat.[(triple5 OR ((triple10) -> rule8))] The lion is big.[(triple6)] The lion is green.[(triple7)] The lion is not nice.[(triple8)] The lion is young.[(triple9)] The lion sees the cat.[(triple10)] @1: The cat is nice.[(((triple3) -> rule5))] @2: The cat does not see the cat.[(((((triple3) -> rule5)) -> rule1))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
triple3
The cat needs the lion.
("cat" "needs" "lion" "+")
triple4
The lion eats the cat.
("lion" "eats" "cat" "+")
triple5
((triple10) -> (rule8 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion is big.
("lion" "is" "big" "+")
triple6
The lion is green.
("lion" "is" "green" "+")
triple7
The lion is not nice.
("lion" "is" "nice" "-")
triple8
The lion is young.
("lion" "is" "young" "+")
triple9
The lion sees the cat.
("lion" "sees" "cat" "+")
triple10
The cat is nice.
("cat" "is" "nice" "+")
((triple3) -> (rule5 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat does not see the cat.
("cat" "sees" "cat" "-")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
The cat does not see the cat.
("cat" "sees" "cat" "-")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2