The dog eats the tiger. The tiger eats the dog. The tiger is blue. If the tiger needs the dog then the tiger eats the dog. If someone is cold then they visit the dog. If someone eats the tiger and the tiger eats the dog then they are cold. If someone eats the tiger and they need the dog then they are green. If someone is red then they are rough. If someone visits the tiger and the tiger eats the dog then the tiger visits the dog.
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If the tiger needs the dog then the tiger eats the dog.
((("tiger" "needs" "dog" "+")) -> ("tiger" "eats" "dog" "+"))
If someone is cold then they visit the dog.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "dog" "+"))
If someone eats the tiger and the tiger eats the dog then they are cold.
((("someone" "eats" "tiger" "+") ("tiger" "eats" "dog" "+")) -> ("someone" "is" "cold" "+"))
If someone eats the tiger and they need the dog then they are green.
((("someone" "eats" "tiger" "+") ("someone" "needs" "dog" "+")) -> ("someone" "is" "green" "+"))
If someone is red then they are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone visits the tiger and the tiger eats the dog then the tiger visits the dog.
((("someone" "visits" "tiger" "+") ("tiger" "eats" "dog" "+")) -> ("tiger" "visits" "dog" "+"))
The tiger eats the dog.
True
1
proof
[(triple2)]
("tiger" "eats" "dog" "+")
triple2
The dog does not eat the tiger.
False
1
inv-proof
[(triple1)]
("dog" "eats" "tiger" "-")
triple1
The dog is cold.
True
3
proof
[(((triple1 triple2) -> rule3))]
("dog" "is" "cold" "+")
((triple1 triple2) -> (rule3 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is not cold.
False
3
inv-proof
[(((triple1 triple2) -> rule3))]
("dog" "is" "cold" "-")
((triple1 triple2) -> (rule3 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog visits the dog.
True
4
proof
[(((((triple1 triple2) -> rule3)) -> rule2))]
("dog" "visits" "dog" "+")
((((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog does not visit the dog.
False
4
inv-proof
[(((((triple1 triple2) -> rule3)) -> rule2))]
("dog" "visits" "dog" "-")
((((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The tiger is not green.
Unknown
inv-rconc
[@1: The tiger is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "green" "-")
The tiger is cold.
Unknown
rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "cold" "+")
The tiger does not visit the dog.
Unknown
inv-rconc
[@2: The tiger visits the dog.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("tiger" "visits" "dog" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The dog does not visit the tiger.
Unknown
inv-random
[@0: The dog visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The dog eats the tiger.[(triple1)] The tiger eats the dog.[(triple2)] The tiger is blue.[(triple3)] @1: The dog is cold.[(((triple1 triple2) -> rule3))] @2: The dog visits the dog.[(((((triple1 triple2) -> rule3)) -> rule2))]
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple2
The tiger is blue.
("tiger" "is" "blue" "+")
triple3
The dog is cold.
("dog" "is" "cold" "+")
((triple1 triple2) -> (rule3 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2