The dog eats the rabbit. The rabbit does not visit the dog. The squirrel visits the rabbit. If someone is young then they chase the dog. If someone is round then they visit the rabbit. If someone visits the rabbit then they are not round.
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The rabbit does not visit the dog.
("rabbit" "visits" "dog" "-")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If someone is young then they chase the dog.
((("someone" "is" "young" "+")) -> ("someone" "chases" "dog" "+"))
If someone is round then they visit the rabbit.
((("someone" "is" "round" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone visits the rabbit then they are not round.
((("someone" "visits" "rabbit" "+")) -> ("someone" "is" "round" "-"))
The dog eats the rabbit.
True
1
proof
[(triple1)]
("dog" "eats" "rabbit" "+")
triple1
The squirrel does not visit the rabbit.
False
1
inv-proof
[(triple3)]
("squirrel" "visits" "rabbit" "-")
triple3
The squirrel is not round.
True
2
proof
[(((triple3) -> rule3))]
("squirrel" "is" "round" "-")
((triple3) -> (rule3 % int1))
The squirrel is not round.
("squirrel" "is" "round" "-")
int1
The squirrel is round.
False
2
inv-proof
[(((triple3) -> rule3))]
("squirrel" "is" "round" "+")
((triple3) -> (rule3 % int1))
The squirrel is not round.
("squirrel" "is" "round" "-")
int1
The rabbit does not chase the dog.
Unknown
inv-rconc
[@1: The rabbit chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "chases" "dog" "-")
The squirrel chases the dog.
Unknown
rconc
[@1: The squirrel chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "dog" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The rabbit eats the squirrel.
Unknown
random
[@0: The rabbit eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "squirrel" "+")
@0: The dog eats the rabbit.[(triple1)] The rabbit does not visit the dog.[(triple2)] The squirrel visits the rabbit.[(triple3)] @1: The squirrel is not round.[(((triple3) -> rule3))]
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple1
The rabbit does not visit the dog.
("rabbit" "visits" "dog" "-")
triple2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple3
The squirrel is not round.
("squirrel" "is" "round" "-")
((triple3) -> (rule3 % int1))
The squirrel is not round.
("squirrel" "is" "round" "-")
int1