The dog eats the tiger. The dog is green. The dog is young. The tiger eats the dog. The tiger is blue. The tiger needs the dog. The tiger sees the dog. If something is green then it sees the tiger. If the tiger needs the dog and the tiger is not cold then the dog eats the tiger.
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is young.
("dog" "is" "young" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If something is green then it sees the tiger.
((("something" "is" "green" "+")) -> ("something" "sees" "tiger" "+"))
If the tiger needs the dog and the tiger is not cold then the dog eats the tiger.
((("tiger" "needs" "dog" "+") ("tiger" "is" "cold" "~")) -> ("dog" "eats" "tiger" "+"))
The dog is green.
True
1
proof
[(triple2)]
("dog" "is" "green" "+")
triple2
The tiger is not blue.
False
1
inv-proof
[(triple5)]
("tiger" "is" "blue" "-")
triple5
The dog sees the tiger.
True
2
proof
[(((triple2) -> rule1))]
("dog" "sees" "tiger" "+")
((triple2) -> (rule1 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The dog does not see the tiger.
False
2
inv-proof
[(((triple2) -> rule1))]
("dog" "sees" "tiger" "-")
((triple2) -> (rule1 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "tiger" "-")
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 eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The dog eats the tiger.[(triple1)] The dog is green.[(triple2)] The dog is young.[(triple3)] The tiger eats the dog.[(triple4)] The tiger is blue.[(triple5)] The tiger needs the dog.[(triple6)] The tiger sees the dog.[(triple7)] @1: The dog sees the tiger.[(((triple2) -> rule1))]
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is young.
("dog" "is" "young" "+")
triple3
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple4
The tiger is blue.
("tiger" "is" "blue" "+")
triple5
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple6
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple7
The dog sees the tiger.
("dog" "sees" "tiger" "+")
((triple2) -> (rule1 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1