The dog eats the tiger. The dog is big. The dog is blue. The dog is nice. The dog sees the tiger. The dog visits the tiger. The tiger is not blue. The tiger is cold. The tiger sees the dog. The tiger visits the dog. If someone is kind then they do not visit the tiger. If someone is kind and they do not eat the tiger then they eat the dog. If someone visits the tiger and they eat the tiger then they eat the dog. If someone sees the tiger then the tiger is kind. If someone visits the dog and they do not see the tiger then they do not see the dog. If someone eats the dog and the dog sees the tiger then they are not cold. If someone eats the tiger and they do not see the dog then the tiger does not eat the dog. If someone is cold then they are big.
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger is not blue.
("tiger" "is" "blue" "-")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If someone is kind then they do not visit the tiger.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "tiger" "-"))
If someone is kind and they do not eat the tiger then they eat the dog.
((("someone" "is" "kind" "+") ("someone" "eats" "tiger" "~")) -> ("someone" "eats" "dog" "+"))
If someone visits the tiger and they eat the tiger then they eat the dog.
((("someone" "visits" "tiger" "+") ("someone" "eats" "tiger" "+")) -> ("someone" "eats" "dog" "+"))
If someone sees the tiger then the tiger is kind.
((("someone" "sees" "tiger" "+")) -> ("tiger" "is" "kind" "+"))
If someone visits the dog and they do not see the tiger then they do not see the dog.
((("someone" "visits" "dog" "+") ("someone" "sees" "tiger" "~")) -> ("someone" "sees" "dog" "-"))
If someone eats the dog and the dog sees the tiger then they are not cold.
((("someone" "eats" "dog" "+") ("dog" "sees" "tiger" "+")) -> ("someone" "is" "cold" "-"))
If someone eats the tiger and they do not see the dog then the tiger does not eat the dog.
((("someone" "eats" "tiger" "+") ("someone" "sees" "dog" "~")) -> ("tiger" "eats" "dog" "-"))
If someone is cold then they are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
The dog is big.
True
1
proof
[(triple2)]
("dog" "is" "big" "+")
triple2
The dog does not visit the tiger.
False
1
inv-proof
[(triple6)]
("dog" "visits" "tiger" "-")
triple6
The dog eats the dog.
True
3
proof
[(((triple6 triple1) -> rule3))]
("dog" "eats" "dog" "+")
((triple6 triple1) -> (rule3 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog does not eat the dog.
False
3
inv-proof
[(((triple6 triple1) -> rule3))]
("dog" "eats" "dog" "-")
((triple6 triple1) -> (rule3 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is not cold.
True
5
proof
[(((((triple6 triple1) -> rule3) triple5) -> rule6))]
("dog" "is" "cold" "-")
((((triple6 triple1) -> (rule3 % int2)) triple5) -> (rule6 % int1))
The dog is not cold.
("dog" "is" "cold" "-")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The tiger visits the tiger.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule1))]
("tiger" "visits" "tiger" "+")
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
The tiger does not visit the tiger.
("tiger" "visits" "tiger" "-")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger does not eat the dog.
Unknown
inv-rconc
[@1: The tiger eats the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "eats" "dog" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog eats the tiger.[(triple1)] The dog is big.[(triple2)] The dog is blue.[(triple3)] The dog is nice.[(triple4)] The dog sees the tiger.[(triple5)] The dog visits the tiger.[(triple6)] The tiger is cold.[(triple8)] The tiger is not blue.[(triple7)] The tiger sees the dog.[(triple9)] The tiger visits the dog.[(triple10)] @1: The dog eats the dog.[(((triple6 triple1) -> rule3))] The tiger is big.[(((triple8) -> rule8))] The tiger is kind.[(((triple5) -> rule4))] @2: The dog is not cold.[(((((triple6 triple1) -> rule3) triple5) -> rule6))] The tiger does not visit the tiger.[(((((triple5) -> rule4)) -> rule1))]
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
triple3
The dog is nice.
("dog" "is" "nice" "+")
triple4
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple5
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple6
The tiger is cold.
("tiger" "is" "cold" "+")
triple8
The tiger is not blue.
("tiger" "is" "blue" "-")
triple7
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple9
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple10
The dog eats the dog.
("dog" "eats" "dog" "+")
((triple6 triple1) -> (rule3 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((triple8) -> (rule8 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple5) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The dog is not cold.
("dog" "is" "cold" "-")
((((triple6 triple1) -> (rule3 % int2)) triple5) -> (rule6 % int1))
The dog is not cold.
("dog" "is" "cold" "-")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The tiger does not visit the tiger.
("tiger" "visits" "tiger" "-")
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
The tiger does not visit the tiger.
("tiger" "visits" "tiger" "-")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2