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