The dog chases the tiger. The dog eats the tiger. The dog is cold. The dog is green. The dog visits the tiger. The tiger chases the dog. The tiger is cold. If something eats the dog and it visits the dog then the dog visits the tiger. All blue things are round. If something chases the dog and it eats the tiger then the tiger visits the dog. If the tiger eats the dog and the tiger chases the dog then the dog visits the tiger. If the dog visits the tiger and the tiger chases the dog then the dog chases the tiger. If something is round and it chases the dog then it eats the tiger. If something chases the tiger then it is round. If the tiger is cold and the tiger chases the dog then the tiger is round.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
If something eats the dog and it visits the dog then the dog visits the tiger.
((("something" "eats" "dog" "+") ("something" "visits" "dog" "+")) -> ("dog" "visits" "tiger" "+"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something chases the dog and it eats the tiger then the tiger visits the dog.
((("something" "chases" "dog" "+") ("something" "eats" "tiger" "+")) -> ("tiger" "visits" "dog" "+"))
If the tiger eats the dog and the tiger chases the dog then the dog visits the tiger.
((("tiger" "eats" "dog" "+") ("tiger" "chases" "dog" "+")) -> ("dog" "visits" "tiger" "+"))
If the dog visits the tiger and the tiger chases the dog then the dog chases the tiger.
((("dog" "visits" "tiger" "+") ("tiger" "chases" "dog" "+")) -> ("dog" "chases" "tiger" "+"))
If something is round and it chases the dog then it eats the tiger.
((("something" "is" "round" "+") ("something" "chases" "dog" "+")) -> ("something" "eats" "tiger" "+"))
If something chases the tiger then it is round.
((("something" "chases" "tiger" "+")) -> ("something" "is" "round" "+"))
If the tiger is cold and the tiger chases the dog then the tiger is round.
((("tiger" "is" "cold" "+") ("tiger" "chases" "dog" "+")) -> ("tiger" "is" "round" "+"))
The tiger chases the dog.
True
1
proof
[(triple6)]
("tiger" "chases" "dog" "+")
triple6
The dog does not eat the tiger.
False
1
inv-proof
[(triple2)]
("dog" "eats" "tiger" "-")
triple2
The dog is round.
True
2
proof
[(((triple1) -> rule7) OR ((((triple5 triple6) -> rule5)) -> rule7))]
("dog" "is" "round" "+")
((triple1) -> (rule7 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
((((triple5 triple6) -> (rule5 % int2))) -> (rule7 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The tiger is not round.
False
3
inv-proof
[(((triple7 triple6) -> rule8))]
("tiger" "is" "round" "-")
((triple7 triple6) -> (rule8 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger eats the tiger.
True
5
proof
[(((((triple7 triple6) -> rule8) triple6) -> rule6))]
("tiger" "eats" "tiger" "+")
((((triple7 triple6) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger does not eat the tiger.
False
5
inv-proof
[(((((triple7 triple6) -> rule8) triple6) -> rule6))]
("tiger" "eats" "tiger" "-")
((((triple7 triple6) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger visits the dog.
True
7
proof
[(((triple6 ((((triple7 triple6) -> rule8) triple6) -> rule6)) -> rule3))]
("tiger" "visits" "dog" "+")
((triple6 ((((triple7 triple6) -> (rule8 % int3)) triple6) -> (rule6 % int2))) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger does not visit the dog.
False
7
inv-proof
[(((triple6 ((((triple7 triple6) -> rule8) triple6) -> rule6)) -> rule3))]
("tiger" "visits" "dog" "-")
((triple6 ((((triple7 triple6) -> (rule8 % int3)) triple6) -> (rule6 % int2))) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger does not eat the dog.
Unknown
inv-random
[@0: The tiger eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "dog" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
@0: The dog chases the tiger.[(triple1 OR ((triple5 triple6) -> rule5))] The dog eats the tiger.[(triple2)] The dog is cold.[(triple3)] The dog is green.[(triple4)] The dog visits the tiger.[(triple5)] The tiger chases the dog.[(triple6)] The tiger is cold.[(triple7)] @1: The dog is round.[(((triple1) -> rule7) OR ((((triple5 triple6) -> rule5)) -> rule7))] The tiger is round.[(((triple7 triple6) -> rule8))] @2: The tiger eats the tiger.[(((((triple7 triple6) -> rule8) triple6) -> rule6))] @3: The tiger visits the dog.[(((triple6 ((((triple7 triple6) -> rule8) triple6) -> rule6)) -> rule3))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
((triple5 triple6) -> (rule5 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple2
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is green.
("dog" "is" "green" "+")
triple4
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple5
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple6
The tiger is cold.
("tiger" "is" "cold" "+")
triple7
The dog is round.
("dog" "is" "round" "+")
((triple1) -> (rule7 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
((((triple5 triple6) -> (rule5 % int2))) -> (rule7 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
((triple7 triple6) -> (rule8 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((triple7 triple6) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
((triple6 ((((triple7 triple6) -> (rule8 % int3)) triple6) -> (rule6 % int2))) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3