The dog eats the tiger. The squirrel is rough. The tiger is round. If something eats the tiger then it sees the tiger. All blue things are rough. If the dog needs the tiger and the dog is blue then the tiger needs the squirrel.
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
If something eats the tiger then it sees the tiger.
((("something" "eats" "tiger" "+")) -> ("something" "sees" "tiger" "+"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If the dog needs the tiger and the dog is blue then the tiger needs the squirrel.
((("dog" "needs" "tiger" "+") ("dog" "is" "blue" "+")) -> ("tiger" "needs" "squirrel" "+"))
The squirrel is rough.
True
1
proof
[(triple2)]
("squirrel" "is" "rough" "+")
triple2
The dog does not eat the tiger.
False
1
inv-proof
[(triple1)]
("dog" "eats" "tiger" "-")
triple1
The dog is not rough.
Unknown
inv-rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "rough" "-")
The squirrel eats the dog.
Unknown
random
[@0: The squirrel eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "dog" "+")
@0: The dog eats the tiger.[(triple1)] The squirrel is rough.[(triple2)] The tiger is round.[(triple3)] @1: The dog sees the tiger.[(((triple1) -> rule1))]
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple1
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple2
The tiger is round.
("tiger" "is" "round" "+")
triple3
The dog sees the tiger.
("dog" "sees" "tiger" "+")
((triple1) -> (rule1 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1