The cat eats the cow. The cat is blue. The cat is nice. The cat is round. The cat needs the cow. The cat visits the cow. The cow eats the cat. The cow is not big. The cow is blue. The cow is kind. The cow is nice. The cow visits the cat. If something visits the cow then it is big. If something needs the cat and it is kind then the cat is not round. If something eats the cow and the cow is round then it eats the cat. If something eats the cow and the cow is not round then it eats the cat. If the cat eats the cow and the cow is not kind then the cow does not need the cat. If something is kind and round then it visits the cow.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow is not big.
("cow" "is" "big" "-")
The cow is blue.
("cow" "is" "blue" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
If something visits the cow then it is big.
((("something" "visits" "cow" "+")) -> ("something" "is" "big" "+"))
If something needs the cat and it is kind then the cat is not round.
((("something" "needs" "cat" "+") ("something" "is" "kind" "+")) -> ("cat" "is" "round" "-"))
If something eats the cow and the cow is round then it eats the cat.
((("something" "eats" "cow" "+") ("cow" "is" "round" "+")) -> ("something" "eats" "cat" "+"))
If something eats the cow and the cow is not round then it eats the cat.
((("something" "eats" "cow" "+") ("cow" "is" "round" "~")) -> ("something" "eats" "cat" "+"))
If the cat eats the cow and the cow is not kind then the cow does not need the cat.
((("cat" "eats" "cow" "+") ("cow" "is" "kind" "~")) -> ("cow" "needs" "cat" "-"))
If something is kind and round then it visits the cow.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "visits" "cow" "+"))
The cat is nice.
True
1
proof
[(triple3)]
("cat" "is" "nice" "+")
triple3
The cow does not eat the cat.
False
1
inv-proof
[(triple7)]
("cow" "eats" "cat" "-")
triple7
The cat is big.
True
2
proof
[(((triple6) -> rule1))]
("cat" "is" "big" "+")
((triple6) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is not big.
False
2
inv-proof
[(((triple6) -> rule1))]
("cat" "is" "big" "-")
((triple6) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat does not eat the cat.
Unknown
inv-rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "eats" "cat" "-")
The cow visits the cow.
Unknown
rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "visits" "cow" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The cat eats the cow.[(triple1)] The cat is blue.[(triple2)] The cat is nice.[(triple3)] The cat is round.[(triple4)] The cat needs the cow.[(triple5)] The cat visits the cow.[(triple6)] The cow eats the cat.[(triple7)] The cow is blue.[(triple9)] The cow is kind.[(triple10)] The cow is nice.[(triple11)] The cow is not big.[(triple8)] The cow visits the cat.[(triple12)] @1: The cat is big.[(((triple6) -> rule1))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat needs the cow.
("cat" "needs" "cow" "+")
triple5
The cat visits the cow.
("cat" "visits" "cow" "+")
triple6
The cow eats the cat.
("cow" "eats" "cat" "+")
triple7
The cow is blue.
("cow" "is" "blue" "+")
triple9
The cow is kind.
("cow" "is" "kind" "+")
triple10
The cow is nice.
("cow" "is" "nice" "+")
triple11
The cow is not big.
("cow" "is" "big" "-")
triple8
The cow visits the cat.
("cow" "visits" "cat" "+")
triple12
The cat is big.
("cat" "is" "big" "+")
((triple6) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1