The dog eats the tiger. The dog is cold. The dog is kind. The dog is nice. The dog needs the tiger. The tiger is nice. The tiger needs the dog. If something needs the dog then the dog is rough. If something needs the dog then it eats the dog. If the tiger eats the dog and the tiger is nice then the dog sees the tiger.
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If something needs the dog then the dog is rough.
((("something" "needs" "dog" "+")) -> ("dog" "is" "rough" "+"))
If something needs the dog then it eats the dog.
((("something" "needs" "dog" "+")) -> ("something" "eats" "dog" "+"))
If the tiger eats the dog and the tiger is nice then the dog sees the tiger.
((("tiger" "eats" "dog" "+") ("tiger" "is" "nice" "+")) -> ("dog" "sees" "tiger" "+"))
The dog is kind.
True
1
proof
[(triple3)]
("dog" "is" "kind" "+")
triple3
The tiger does not need the dog.
False
1
inv-proof
[(triple7)]
("tiger" "needs" "dog" "-")
triple7
The tiger eats the dog.
True
2
proof
[(((triple7) -> rule2))]
("tiger" "eats" "dog" "+")
((triple7) -> (rule2 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The dog is not rough.
False
2
inv-proof
[(((triple7) -> rule1))]
("dog" "is" "rough" "-")
((triple7) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog sees the tiger.
True
4
proof
[(((((triple7) -> rule2) triple6) -> rule3))]
("dog" "sees" "tiger" "+")
((((triple7) -> (rule2 % int2)) triple6) -> (rule3 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2
The dog does not see the tiger.
False
4
inv-proof
[(((((triple7) -> rule2) triple6) -> rule3))]
("dog" "sees" "tiger" "-")
((((triple7) -> (rule2 % int2)) triple6) -> (rule3 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "dog" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The tiger sees the dog.
Unknown
random
[@0: The tiger sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "dog" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The dog eats the tiger.[(triple1)] The dog is cold.[(triple2)] The dog is kind.[(triple3)] The dog is nice.[(triple4)] The dog needs the tiger.[(triple5)] The tiger is nice.[(triple6)] The tiger needs the dog.[(triple7)] @1: The dog is rough.[(((triple7) -> rule1))] The tiger eats the dog.[(((triple7) -> rule2))] @2: The dog sees the tiger.[(((((triple7) -> rule2) triple6) -> rule3))]
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog is nice.
("dog" "is" "nice" "+")
triple4
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple5
The tiger is nice.
("tiger" "is" "nice" "+")
triple6
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple7
The dog is rough.
("dog" "is" "rough" "+")
((triple7) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
((triple7) -> (rule2 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
((((triple7) -> (rule2 % int2)) triple6) -> (rule3 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2