The cat eats the squirrel. The cat is cold. The dog eats the squirrel. The squirrel is young. The squirrel sees the cat. The squirrel visits the cat. The squirrel visits the dog. If something visits the squirrel and it eats the dog then the dog sees the squirrel. If something is young then it visits the dog. If the squirrel eats the dog and the dog is young then the squirrel is kind. If something visits the dog then the dog sees the cat. If something eats the squirrel and it sees the cat then it eats the cat. If something visits the cat and it is young then the cat visits the squirrel. If something visits the squirrel then it is young. If the squirrel is young then the squirrel is round.
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is cold.
("cat" "is" "cold" "+")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If something visits the squirrel and it eats the dog then the dog sees the squirrel.
((("something" "visits" "squirrel" "+") ("something" "eats" "dog" "+")) -> ("dog" "sees" "squirrel" "+"))
If something is young then it visits the dog.
((("something" "is" "young" "+")) -> ("something" "visits" "dog" "+"))
If the squirrel eats the dog and the dog is young then the squirrel is kind.
((("squirrel" "eats" "dog" "+") ("dog" "is" "young" "+")) -> ("squirrel" "is" "kind" "+"))
If something visits the dog then the dog sees the cat.
((("something" "visits" "dog" "+")) -> ("dog" "sees" "cat" "+"))
If something eats the squirrel and it sees the cat then it eats the cat.
((("something" "eats" "squirrel" "+") ("something" "sees" "cat" "+")) -> ("something" "eats" "cat" "+"))
If something visits the cat and it is young then the cat visits the squirrel.
((("something" "visits" "cat" "+") ("something" "is" "young" "+")) -> ("cat" "visits" "squirrel" "+"))
If something visits the squirrel then it is young.
((("something" "visits" "squirrel" "+")) -> ("something" "is" "young" "+"))
If the squirrel is young then the squirrel is round.
((("squirrel" "is" "young" "+")) -> ("squirrel" "is" "round" "+"))
The squirrel visits the cat.
True
1
proof
[(triple6)]
("squirrel" "visits" "cat" "+")
triple6
The squirrel does not visit the cat.
False
1
inv-proof
[(triple6)]
("squirrel" "visits" "cat" "-")
triple6
The squirrel is round.
True
2
proof
[(((triple4) -> rule8))]
("squirrel" "is" "round" "+")
((triple4) -> (rule8 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is not round.
False
2
inv-proof
[(((triple4) -> rule8))]
("squirrel" "is" "round" "-")
((triple4) -> (rule8 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The cat is young.
True
4
proof
[(((((triple6 triple4) -> rule6)) -> rule7))]
("cat" "is" "young" "+")
((((triple6 triple4) -> (rule6 % int2))) -> (rule7 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The dog does not eat the cat.
False
4
inv-proof
[(((triple3 ((triple7) -> rule4)) -> rule5) OR ((triple3 ((((triple4) -> rule2)) -> rule4)) -> rule5) OR ((triple3 ((((((((triple6 triple4) -> rule6)) -> rule7)) -> rule2)) -> rule4)) -> rule5))]
("dog" "eats" "cat" "-")
((triple3 ((triple7) -> (rule4 % int2))) -> (rule5 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
((triple3 ((((triple4) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int3
((triple3 ((((((((triple6 triple4) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int5
The cat visits the dog.
True
5
proof
[(((((((triple6 triple4) -> rule6)) -> rule7)) -> rule2))]
("cat" "visits" "dog" "+")
((((((triple6 triple4) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int3
The cat does not visit the dog.
False
5
inv-proof
[(((((((triple6 triple4) -> rule6)) -> rule7)) -> rule2))]
("cat" "visits" "dog" "-")
((((((triple6 triple4) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int3
The dog does not visit the dog.
Unknown
inv-rconc
[@2: The dog visits the dog.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("dog" "visits" "dog" "-")
The dog sees the squirrel.
Unknown
rconc
[@1: The dog sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "squirrel" "+")
The squirrel does not eat the cat.
Unknown
inv-rconc
[@1: The squirrel eats the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "eats" "cat" "-")
The dog is young.
Unknown
rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "young" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The dog visits the squirrel.
Unknown
random
[@0: The dog visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "squirrel" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The cat sees the dog.
Unknown
random
[@0: The cat sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "dog" "+")
@0: The cat eats the squirrel.[(triple1)] The cat is cold.[(triple2)] The dog eats the squirrel.[(triple3)] The squirrel is young.[(triple4)] The squirrel sees the cat.[(triple5)] The squirrel visits the cat.[(triple6)] The squirrel visits the dog.[(triple7 OR ((triple4) -> rule2))] @1: The cat visits the squirrel.[(((triple6 triple4) -> rule6))] The dog sees the cat.[(((triple7) -> rule4) OR ((((triple4) -> rule2)) -> rule4) OR ((((((((triple6 triple4) -> rule6)) -> rule7)) -> rule2)) -> rule4))] The squirrel is round.[(((triple4) -> rule8))] @2: The cat is young.[(((((triple6 triple4) -> rule6)) -> rule7))] The dog eats the cat.[(((triple3 ((triple7) -> rule4)) -> rule5) OR ((triple3 ((((triple4) -> rule2)) -> rule4)) -> rule5) OR ((triple3 ((((((((triple6 triple4) -> rule6)) -> rule7)) -> rule2)) -> rule4)) -> rule5))] @3: The cat visits the dog.[(((((((triple6 triple4) -> rule6)) -> rule7)) -> rule2))]
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple3
The squirrel is young.
("squirrel" "is" "young" "+")
triple4
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple5
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple6
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple7
((triple4) -> (rule2 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
((triple6 triple4) -> (rule6 % int1))
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
((triple7) -> (rule4 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule4 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
((((((((triple6 triple4) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int4
The squirrel is round.
("squirrel" "is" "round" "+")
((triple4) -> (rule8 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((((triple6 triple4) -> (rule6 % int2))) -> (rule7 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The dog eats the cat.
("dog" "eats" "cat" "+")
((triple3 ((triple7) -> (rule4 % int2))) -> (rule5 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
((triple3 ((((triple4) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int3
((triple3 ((((((((triple6 triple4) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int5
The cat visits the dog.
("cat" "visits" "dog" "+")
((((((triple6 triple4) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int3