The cow eats the tiger. The cow is rough. The cow likes the tiger. The squirrel visits the cow. The tiger is big. The tiger visits the cow. The tiger visits the squirrel. If something eats the tiger then it is young. All young things are cold. If something likes the squirrel then it is cold. If something is young and it visits the tiger then it is big. If something visits the cow then it is big. If the tiger visits the cow and the cow is young then the cow is big. If something visits the cow then it eats the tiger. If the squirrel likes the tiger and the squirrel eats the tiger then the squirrel eats the cow.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If something eats the tiger then it is young.
((("something" "eats" "tiger" "+")) -> ("something" "is" "young" "+"))
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something likes the squirrel then it is cold.
((("something" "likes" "squirrel" "+")) -> ("something" "is" "cold" "+"))
If something is young and it visits the tiger then it is big.
((("something" "is" "young" "+") ("something" "visits" "tiger" "+")) -> ("something" "is" "big" "+"))
If something visits the cow then it is big.
((("something" "visits" "cow" "+")) -> ("something" "is" "big" "+"))
If the tiger visits the cow and the cow is young then the cow is big.
((("tiger" "visits" "cow" "+") ("cow" "is" "young" "+")) -> ("cow" "is" "big" "+"))
If something visits the cow then it eats the tiger.
((("something" "visits" "cow" "+")) -> ("something" "eats" "tiger" "+"))
If the squirrel likes the tiger and the squirrel eats the tiger then the squirrel eats the cow.
((("squirrel" "likes" "tiger" "+") ("squirrel" "eats" "tiger" "+")) -> ("squirrel" "eats" "cow" "+"))
The cow eats the tiger.
True
1
proof
[(triple1)]
("cow" "eats" "tiger" "+")
triple1
The tiger does not visit the squirrel.
False
1
inv-proof
[(triple7)]
("tiger" "visits" "squirrel" "-")
triple7
The squirrel eats the tiger.
True
2
proof
[(((triple4) -> rule7))]
("squirrel" "eats" "tiger" "+")
((triple4) -> (rule7 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The tiger does not eat the tiger.
False
2
inv-proof
[(((triple6) -> rule7))]
("tiger" "eats" "tiger" "-")
((triple6) -> (rule7 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The cow is big.
True
4
proof
[(((triple6 ((triple1) -> rule1)) -> rule6))]
("cow" "is" "big" "+")
((triple6 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The tiger is not young.
False
3
inv-proof
[(((((triple6) -> rule7)) -> rule1))]
("tiger" "is" "young" "-")
((((triple6) -> (rule7 % int2))) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The squirrel is cold.
True
4
proof
[(((((((triple4) -> rule7)) -> rule1)) -> rule2))]
("squirrel" "is" "cold" "+")
((((((triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
The squirrel is not cold.
False
4
inv-proof
[(((((((triple4) -> rule7)) -> rule1)) -> rule2))]
("squirrel" "is" "cold" "-")
((((((triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
The squirrel does not eat the cow.
Unknown
inv-rconc
[@1: The squirrel eats the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "eats" "cow" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The tiger likes the squirrel.
Unknown
random
[@0: The tiger likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "squirrel" "+")
The squirrel does not like the cow.
Unknown
inv-random
[@0: The squirrel likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "cow" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
@0: The cow eats the tiger.[(triple1)] The cow is rough.[(triple2)] The cow likes the tiger.[(triple3)] The squirrel visits the cow.[(triple4)] The tiger is big.[(triple5 OR ((triple6) -> rule5))] The tiger visits the cow.[(triple6)] The tiger visits the squirrel.[(triple7)] @1: The cow is young.[(((triple1) -> rule1))] The squirrel eats the tiger.[(((triple4) -> rule7))] The squirrel is big.[(((triple4) -> rule5))] The tiger eats the tiger.[(((triple6) -> rule7))] @2: The cow is big.[(((triple6 ((triple1) -> rule1)) -> rule6))] The cow is cold.[(((((triple1) -> rule1)) -> rule2))] The squirrel is young.[(((((triple4) -> rule7)) -> rule1))] The tiger is young.[(((((triple6) -> rule7)) -> rule1))] @3: The squirrel is cold.[(((((((triple4) -> rule7)) -> rule1)) -> rule2))] The tiger is cold.[(((((((triple6) -> rule7)) -> rule1)) -> rule2))]
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
triple2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple3
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple4
The tiger is big.
("tiger" "is" "big" "+")
triple5
((triple6) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple6
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple7
The cow is young.
("cow" "is" "young" "+")
((triple1) -> (rule1 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
((triple4) -> (rule7 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((triple4) -> (rule5 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple6) -> (rule7 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The cow is big.
("cow" "is" "big" "+")
((triple6 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
((((triple4) -> (rule7 % int2))) -> (rule1 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
((((triple6) -> (rule7 % int2))) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((((triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
((((((triple6) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3