The cat eats the tiger. The cat is red. The cat sees the cow. The cow is big. The cow sees the squirrel. The cow does not see the tiger. The squirrel is not kind. The squirrel visits the cow. The tiger is red. The tiger sees the cow. If something eats the tiger then the tiger is young. If something sees the cow then it visits the cow. If something is round then it visits the cow. Big things are not young. If the tiger is round and the tiger is not big then the tiger visits the squirrel. If something is young then it visits the tiger. If something sees the cat and the cat eats the tiger then the cat sees the cow. If something visits the tiger then it sees the tiger.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is red.
("cat" "is" "red" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow is big.
("cow" "is" "big" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The cow does not see the tiger.
("cow" "sees" "tiger" "-")
The squirrel is not kind.
("squirrel" "is" "kind" "-")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If something eats the tiger then the tiger is young.
((("something" "eats" "tiger" "+")) -> ("tiger" "is" "young" "+"))
If something sees the cow then it visits the cow.
((("something" "sees" "cow" "+")) -> ("something" "visits" "cow" "+"))
If something is round then it visits the cow.
((("something" "is" "round" "+")) -> ("something" "visits" "cow" "+"))
Big things are not young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "-"))
If the tiger is round and the tiger is not big then the tiger visits the squirrel.
((("tiger" "is" "round" "+") ("tiger" "is" "big" "~")) -> ("tiger" "visits" "squirrel" "+"))
If something is young then it visits the tiger.
((("something" "is" "young" "+")) -> ("something" "visits" "tiger" "+"))
If something sees the cat and the cat eats the tiger then the cat sees the cow.
((("something" "sees" "cat" "+") ("cat" "eats" "tiger" "+")) -> ("cat" "sees" "cow" "+"))
If something visits the tiger then it sees the tiger.
((("something" "visits" "tiger" "+")) -> ("something" "sees" "tiger" "+"))
The cat eats the tiger.
True
1
proof
[(triple1)]
("cat" "eats" "tiger" "+")
triple1
The cat does not eat the tiger.
False
1
inv-proof
[(triple1)]
("cat" "eats" "tiger" "-")
triple1
The cat visits the cow.
True
2
proof
[(((triple3) -> rule2))]
("cat" "visits" "cow" "+")
((triple3) -> (rule2 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The tiger does not visit the cow.
False
2
inv-proof
[(((triple10) -> rule2))]
("tiger" "visits" "cow" "-")
((triple10) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger visits the tiger.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("tiger" "visits" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger does not visit the tiger.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("tiger" "visits" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger sees the tiger.
True
4
proof
[(((((((triple1) -> rule1)) -> rule6)) -> rule8))]
("tiger" "sees" "tiger" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger does not see the tiger.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule6)) -> rule8))]
("tiger" "sees" "tiger" "-")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The cat does not visit the tiger.
Unknown
inv-rconc
[@1: The cat visits the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "visits" "tiger" "-")
The squirrel visits the tiger.
Unknown
rconc
[@1: The squirrel visits the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "visits" "tiger" "+")
The cat does not see the tiger.
Unknown
inv-rconc
[@2: The cat sees the tiger.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("cat" "sees" "tiger" "-")
The tiger visits the squirrel.
Unknown
rconc
[@1: The tiger visits the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "visits" "squirrel" "+")
The squirrel does not see the cat.
Unknown
inv-random
[@0: The squirrel sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "cat" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
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 is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
@0: The cat eats the tiger.[(triple1)] The cat is red.[(triple2)] The cat sees the cow.[(triple3)] The cow does not see the tiger.[(triple6)] The cow is big.[(triple4)] The cow sees the squirrel.[(triple5)] The squirrel is not kind.[(triple7)] The squirrel visits the cow.[(triple8)] The tiger is red.[(triple9)] The tiger sees the cow.[(triple10)] @1: The cat visits the cow.[(((triple3) -> rule2))] The cow is not young.[(((triple4) -> rule4))] The tiger is young.[(((triple1) -> rule1))] The tiger visits the cow.[(((triple10) -> rule2))] @2: The tiger visits the tiger.[(((((triple1) -> rule1)) -> rule6))] @3: The tiger sees the tiger.[(((((((triple1) -> rule1)) -> rule6)) -> rule8))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The cat sees the cow.
("cat" "sees" "cow" "+")
triple3
The cow does not see the tiger.
("cow" "sees" "tiger" "-")
triple6
The cow is big.
("cow" "is" "big" "+")
triple4
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple5
The squirrel is not kind.
("squirrel" "is" "kind" "-")
triple7
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple8
The tiger is red.
("tiger" "is" "red" "+")
triple9
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple10
The cat visits the cow.
("cat" "visits" "cow" "+")
((triple3) -> (rule2 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cow is not young.
("cow" "is" "young" "-")
((triple4) -> (rule4 % int1))
The cow is not young.
("cow" "is" "young" "-")
int1
The tiger is young.
("tiger" "is" "young" "+")
((triple1) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
((triple10) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3