The cat is round. The cat sees the cow. The cat visits the cow. The cow is big. The cow needs the cat. The rabbit is red. The rabbit visits the cat. The squirrel needs the cat. The squirrel needs the cow. The squirrel needs the rabbit. If someone is big then they visit the cow.
The cat is round.
("cat" "is" "round" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow is big.
("cow" "is" "big" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
If someone is big then they visit the cow.
((("someone" "is" "big" "+")) -> ("someone" "visits" "cow" "+"))
The cat sees the cow.
True
1
proof
[(triple2)]
("cat" "sees" "cow" "+")
triple2
The cat does not see the cow.
False
1
inv-proof
[(triple2)]
("cat" "sees" "cow" "-")
triple2
The cow visits the cow.
True
2
proof
[(((triple4) -> rule1))]
("cow" "visits" "cow" "+")
((triple4) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow does not visit the cow.
False
2
inv-proof
[(((triple4) -> rule1))]
("cow" "visits" "cow" "-")
((triple4) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The rabbit does not visit the cow.
Unknown
inv-rconc
[@1: The rabbit visits the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "cow" "-")
The squirrel visits the cow.
Unknown
rconc
[@1: The squirrel visits the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "visits" "cow" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The squirrel visits the rabbit.
Unknown
random
[@0: The squirrel visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "rabbit" "+")
@0: The cat is round.[(triple1)] The cat sees the cow.[(triple2)] The cat visits the cow.[(triple3)] The cow is big.[(triple4)] The cow needs the cat.[(triple5)] The rabbit is red.[(triple6)] The rabbit visits the cat.[(triple7)] The squirrel needs the cat.[(triple8)] The squirrel needs the cow.[(triple9)] The squirrel needs the rabbit.[(triple10)] @1: The cow visits the cow.[(((triple4) -> rule1))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cat sees the cow.
("cat" "sees" "cow" "+")
triple2
The cat visits the cow.
("cat" "visits" "cow" "+")
triple3
The cow is big.
("cow" "is" "big" "+")
triple4
The cow needs the cat.
("cow" "needs" "cat" "+")
triple5
The rabbit is red.
("rabbit" "is" "red" "+")
triple6
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple7
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple8
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple9
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple10
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple4) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1