The cat is big. The cat needs the cow. The cat visits the tiger. The cow eats the lion. The cow eats the tiger. The cow is rough. The lion eats the cat. The tiger eats the cow. The tiger is blue. The tiger visits the lion. If something visits the tiger then it needs the cat. If something is rough then it visits the lion. If something eats the lion then it is blue. If something needs the cow then the cow eats the cat. If something is blue then it is green. If the tiger is blue and the tiger visits the cat then the tiger eats the cow. If something eats the lion and it needs the tiger then the tiger is rough. If something visits the cat then it is big.
The cat is big.
("cat" "is" "big" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is rough.
("cow" "is" "rough" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If something visits the tiger then it needs the cat.
((("something" "visits" "tiger" "+")) -> ("something" "needs" "cat" "+"))
If something is rough then it visits the lion.
((("something" "is" "rough" "+")) -> ("something" "visits" "lion" "+"))
If something eats the lion then it is blue.
((("something" "eats" "lion" "+")) -> ("something" "is" "blue" "+"))
If something needs the cow then the cow eats the cat.
((("something" "needs" "cow" "+")) -> ("cow" "eats" "cat" "+"))
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If the tiger is blue and the tiger visits the cat then the tiger eats the cow.
((("tiger" "is" "blue" "+") ("tiger" "visits" "cat" "+")) -> ("tiger" "eats" "cow" "+"))
If something eats the lion and it needs the tiger then the tiger is rough.
((("something" "eats" "lion" "+") ("something" "needs" "tiger" "+")) -> ("tiger" "is" "rough" "+"))
If something visits the cat then it is big.
((("something" "visits" "cat" "+")) -> ("something" "is" "big" "+"))
The cow is rough.
True
1
proof
[(triple6)]
("cow" "is" "rough" "+")
triple6
The tiger is not blue.
False
1
inv-proof
[(triple9)]
("tiger" "is" "blue" "-")
triple9
The cat needs the cat.
True
2
proof
[(((triple3) -> rule1))]
("cat" "needs" "cat" "+")
((triple3) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cow does not eat the cat.
False
2
inv-proof
[(((triple2) -> rule4))]
("cow" "eats" "cat" "-")
((triple2) -> (rule4 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The cow is green.
True
3
proof
[(((((triple4) -> rule3)) -> rule5))]
("cow" "is" "green" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is not green.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule5))]
("cow" "is" "green" "-")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The tiger is not rough.
Unknown
inv-rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "is" "rough" "-")
The cow is big.
Unknown
rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "is" "big" "+")
The lion is not green.
Unknown
inv-rconc
[@2: The lion is green.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("lion" "is" "green" "-")
The cat needs the lion.
Unknown
random
[@0: The cat needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "lion" "+")
The tiger does not eat the cat.
Unknown
inv-random
[@0: The tiger eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "cat" "-")
The tiger visits the cow.
Unknown
random
[@0: The tiger visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "cow" "+")
@0: The cat is big.[(triple1)] The cat needs the cow.[(triple2)] The cat visits the tiger.[(triple3)] The cow eats the lion.[(triple4)] The cow eats the tiger.[(triple5)] The cow is rough.[(triple6)] The lion eats the cat.[(triple7)] The tiger eats the cow.[(triple8)] The tiger is blue.[(triple9)] The tiger visits the lion.[(triple10)] @1: The cat needs the cat.[(((triple3) -> rule1))] The cow eats the cat.[(((triple2) -> rule4))] The cow is blue.[(((triple4) -> rule3))] The cow visits the lion.[(((triple6) -> rule2))] The tiger is green.[(((triple9) -> rule5))] @2: The cow is green.[(((((triple4) -> rule3)) -> rule5))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat needs the cow.
("cat" "needs" "cow" "+")
triple2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple3
The cow eats the lion.
("cow" "eats" "lion" "+")
triple4
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple5
The cow is rough.
("cow" "is" "rough" "+")
triple6
The lion eats the cat.
("lion" "eats" "cat" "+")
triple7
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple10
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple3) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
((triple2) -> (rule4 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
((triple4) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
((triple6) -> (rule2 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
((triple9) -> (rule5 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The cow is green.
("cow" "is" "green" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2