The cat chases the lion. The cat needs the lion. The cow does not chase the cat. The cow chases the lion. The cow eats the lion. The cow is kind. The cow needs the lion. The lion chases the cat. The lion chases the cow. The lion is blue. The lion is not green. The lion is kind. The lion is round. The lion needs the cat. The lion needs the cow. If something needs the cat then the cat chases the cow. If something chases the cow then it eats the lion. If something eats the cow and the cow chases the cat then the cat is blue. If the lion does not chase the cat then the lion does not chase the cow. If something eats the lion and it needs the cat then it chases the cow. If something needs the lion then it does not eat the cat.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cow does not chase the cat.
("cow" "chases" "cat" "-")
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is not green.
("lion" "is" "green" "-")
The lion is kind.
("lion" "is" "kind" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
If something needs the cat then the cat chases the cow.
((("something" "needs" "cat" "+")) -> ("cat" "chases" "cow" "+"))
If something chases the cow then it eats the lion.
((("something" "chases" "cow" "+")) -> ("something" "eats" "lion" "+"))
If something eats the cow and the cow chases the cat then the cat is blue.
((("something" "eats" "cow" "+") ("cow" "chases" "cat" "+")) -> ("cat" "is" "blue" "+"))
If the lion does not chase the cat then the lion does not chase the cow.
((("lion" "chases" "cat" "~")) -> ("lion" "chases" "cow" "-"))
If something eats the lion and it needs the cat then it chases the cow.
((("something" "eats" "lion" "+") ("something" "needs" "cat" "+")) -> ("something" "chases" "cow" "+"))
If something needs the lion then it does not eat the cat.
((("something" "needs" "lion" "+")) -> ("something" "eats" "cat" "-"))
The lion is round.
True
1
proof
[(triple13)]
("lion" "is" "round" "+")
triple13
The lion is green.
False
1
inv-proof
[(triple11)]
("lion" "is" "green" "+")
triple11
The lion eats the lion.
True
2
proof
[(((triple9) -> rule2))]
("lion" "eats" "lion" "+")
((triple9) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion does not eat the lion.
False
2
inv-proof
[(((triple9) -> rule2))]
("lion" "eats" "lion" "-")
((triple9) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The cat eats the lion.
True
3
proof
[(((((triple14) -> rule1)) -> rule2))]
("cat" "eats" "lion" "+")
((((triple14) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cat does not eat the lion.
False
3
inv-proof
[(((((triple14) -> rule1)) -> rule2))]
("cat" "eats" "lion" "-")
((((triple14) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "chases" "cow" "-")
The cat is blue.
Unknown
rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "blue" "+")
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 lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The cow does not need the cat.
Unknown
inv-random
[@0: The cow needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cat" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
@0: The cat chases the lion.[(triple1)] The cat needs the lion.[(triple2)] The cow chases the lion.[(triple4)] The cow does not chase the cat.[(triple3)] The cow eats the lion.[(triple5)] The cow is kind.[(triple6)] The cow needs the lion.[(triple7)] The lion chases the cat.[(triple8)] The lion chases the cow.[(triple9)] The lion is blue.[(triple10)] The lion is kind.[(triple12)] The lion is not green.[(triple11)] The lion is round.[(triple13)] The lion needs the cat.[(triple14)] The lion needs the cow.[(triple15)] @1: The cat chases the cow.[(((triple14) -> rule1))] The cat does not eat the cat.[(((triple2) -> rule6))] The cow does not eat the cat.[(((triple7) -> rule6))] The lion eats the lion.[(((triple9) -> rule2))] @2: The cat eats the lion.[(((((triple14) -> rule1)) -> rule2))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat needs the lion.
("cat" "needs" "lion" "+")
triple2
The cow chases the lion.
("cow" "chases" "lion" "+")
triple4
The cow does not chase the cat.
("cow" "chases" "cat" "-")
triple3
The cow eats the lion.
("cow" "eats" "lion" "+")
triple5
The cow is kind.
("cow" "is" "kind" "+")
triple6
The cow needs the lion.
("cow" "needs" "lion" "+")
triple7
The lion chases the cat.
("lion" "chases" "cat" "+")
triple8
The lion chases the cow.
("lion" "chases" "cow" "+")
triple9
The lion is blue.
("lion" "is" "blue" "+")
triple10
The lion is kind.
("lion" "is" "kind" "+")
triple12
The lion is not green.
("lion" "is" "green" "-")
triple11
The lion is round.
("lion" "is" "round" "+")
triple13
The lion needs the cat.
("lion" "needs" "cat" "+")
triple14
The lion needs the cow.
("lion" "needs" "cow" "+")
triple15
The cat chases the cow.
("cat" "chases" "cow" "+")
((triple14) -> (rule1 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat does not eat the cat.
("cat" "eats" "cat" "-")
((triple2) -> (rule6 % int1))
The cat does not eat the cat.
("cat" "eats" "cat" "-")
int1
The cow does not eat the cat.
("cow" "eats" "cat" "-")
((triple7) -> (rule6 % int1))
The cow does not eat the cat.
("cow" "eats" "cat" "-")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple9) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
((((triple14) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2