The cat eats the squirrel. The squirrel visits the cat. If someone eats the squirrel and they visit the squirrel then they are big. If someone is big then they chase the squirrel. If someone is round then they visit the cat. If someone visits the squirrel and they chase the cat then the cat eats the squirrel. If someone visits the cat then the cat visits the squirrel. If someone is big then they eat the squirrel. If someone eats the squirrel then the squirrel eats the cat. If someone visits the cat then they eat the cat.
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
If someone eats the squirrel and they visit the squirrel then they are big.
((("someone" "eats" "squirrel" "+") ("someone" "visits" "squirrel" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they chase the squirrel.
((("someone" "is" "big" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone is round then they visit the cat.
((("someone" "is" "round" "+")) -> ("someone" "visits" "cat" "+"))
If someone visits the squirrel and they chase the cat then the cat eats the squirrel.
((("someone" "visits" "squirrel" "+") ("someone" "chases" "cat" "+")) -> ("cat" "eats" "squirrel" "+"))
If someone visits the cat then the cat visits the squirrel.
((("someone" "visits" "cat" "+")) -> ("cat" "visits" "squirrel" "+"))
If someone is big then they eat the squirrel.
((("someone" "is" "big" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone eats the squirrel then the squirrel eats the cat.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "eats" "cat" "+"))
If someone visits the cat then they eat the cat.
((("someone" "visits" "cat" "+")) -> ("someone" "eats" "cat" "+"))
The cat eats the squirrel.
True
1
proof
[(triple1)]
("cat" "eats" "squirrel" "+")
triple1
The cat does not eat the squirrel.
False
1
inv-proof
[(triple1)]
("cat" "eats" "squirrel" "-")
triple1
The squirrel eats the cat.
True
2
proof
[(((triple1) -> rule7) OR ((triple2) -> rule8))]
("squirrel" "eats" "cat" "+")
((triple1) -> (rule7 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
((triple2) -> (rule8 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel does not eat the cat.
False
2
inv-proof
[(((triple1) -> rule7) OR ((triple2) -> rule8))]
("squirrel" "eats" "cat" "-")
((triple1) -> (rule7 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
((triple2) -> (rule8 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cat is big.
True
4
proof
[(((triple1 ((triple2) -> rule5)) -> rule1))]
("cat" "is" "big" "+")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The cat is not big.
False
4
inv-proof
[(((triple1 ((triple2) -> rule5)) -> rule1))]
("cat" "is" "big" "-")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The squirrel is not big.
Unknown
inv-rconc
[@1: The squirrel is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "big" "-")
The squirrel eats the squirrel.
Unknown
rconc
[@2: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("squirrel" "eats" "squirrel" "+")
The cat does not eat the cat.
Unknown
inv-rconc
[@2: The cat eats the cat.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("cat" "eats" "cat" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The squirrel chases the cat.
Unknown
random
[@0: The squirrel chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "cat" "+")
@0: The cat eats the squirrel.[(triple1)] The squirrel visits the cat.[(triple2)] @1: The cat visits the squirrel.[(((triple2) -> rule5))] The squirrel eats the cat.[(((triple1) -> rule7) OR ((triple2) -> rule8))] @2: The cat is big.[(((triple1 ((triple2) -> rule5)) -> rule1))] @3: The cat chases the squirrel.[(((((triple1 ((triple2) -> rule5)) -> rule1)) -> rule2))]
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
((triple2) -> (rule5 % int1))
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
((triple1) -> (rule7 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
((triple2) -> (rule8 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The cat is big.
("cat" "is" "big" "+")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
((((triple1 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int3