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