The cow chases the tiger. The cow is cold. The cow is red. The cow needs the dog. The dog chases the tiger. The dog needs the cow. The dog visits the tiger. The tiger chases the cow. The tiger is cold. The tiger needs the dog. If the dog is cold then the dog chases the cow. If someone needs the tiger then the tiger visits the cow. If the dog visits the cow and the cow chases the dog then the cow visits the dog. If someone chases the cow then they are nice. If someone is cold then they chase the dog. If someone chases the dog and the dog needs the cow then the dog is young. If someone is cold then they need the tiger. If the cow is red then the cow chases the dog.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is red.
("cow" "is" "red" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If the dog is cold then the dog chases the cow.
((("dog" "is" "cold" "+")) -> ("dog" "chases" "cow" "+"))
If someone needs the tiger then the tiger visits the cow.
((("someone" "needs" "tiger" "+")) -> ("tiger" "visits" "cow" "+"))
If the dog visits the cow and the cow chases the dog then the cow visits the dog.
((("dog" "visits" "cow" "+") ("cow" "chases" "dog" "+")) -> ("cow" "visits" "dog" "+"))
If someone chases the cow then they are nice.
((("someone" "chases" "cow" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold then they chase the dog.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "dog" "+"))
If someone chases the dog and the dog needs the cow then the dog is young.
((("someone" "chases" "dog" "+") ("dog" "needs" "cow" "+")) -> ("dog" "is" "young" "+"))
If someone is cold then they need the tiger.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "tiger" "+"))
If the cow is red then the cow chases the dog.
((("cow" "is" "red" "+")) -> ("cow" "chases" "dog" "+"))
The tiger needs the dog.
True
1
proof
[(triple10)]
("tiger" "needs" "dog" "+")
triple10
The cow does not chase the tiger.
False
1
inv-proof
[(triple1)]
("cow" "chases" "tiger" "-")
triple1
The cow chases the dog.
True
2
proof
[(((triple2) -> rule5) OR ((triple3) -> rule8))]
("cow" "chases" "dog" "+")
((triple2) -> (rule5 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
((triple3) -> (rule8 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow does not need the tiger.
False
2
inv-proof
[(((triple2) -> rule7))]
("cow" "needs" "tiger" "-")
((triple2) -> (rule7 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The dog is young.
True
4
proof
[(((((triple2) -> rule5) triple6) -> rule6) OR ((((triple3) -> rule8) triple6) -> rule6) OR ((((triple9) -> rule5) triple6) -> rule6))]
("dog" "is" "young" "+")
((((triple2) -> (rule5 % int2)) triple6) -> (rule6 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
((((triple3) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
((((triple9) -> (rule5 % int2)) triple6) -> (rule6 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The tiger does not visit the cow.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule2) OR ((((triple9) -> rule7)) -> rule2))]
("tiger" "visits" "cow" "-")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
((((triple9) -> (rule7 % int2))) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "chases" "dog" "-")
The dog is nice.
Unknown
rconc
[@2: The dog is nice.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("dog" "is" "nice" "+")
The dog does not chase the cow.
Unknown
inv-rconc
[@1: The dog chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "cow" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
The cow does not visit the tiger.
Unknown
inv-random
[@0: The cow visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "tiger" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
@0: The cow chases the tiger.[(triple1)] The cow is cold.[(triple2)] The cow is red.[(triple3)] The cow needs the dog.[(triple4)] The dog chases the tiger.[(triple5)] The dog needs the cow.[(triple6)] The dog visits the tiger.[(triple7)] The tiger chases the cow.[(triple8)] The tiger is cold.[(triple9)] The tiger needs the dog.[(triple10)] @1: The cow chases the dog.[(((triple2) -> rule5) OR ((triple3) -> rule8))] The cow needs the tiger.[(((triple2) -> rule7))] The tiger chases the dog.[(((triple9) -> rule5))] The tiger is nice.[(((triple8) -> rule4))] The tiger needs the tiger.[(((triple9) -> rule7))] @2: The dog is young.[(((((triple2) -> rule5) triple6) -> rule6) OR ((((triple3) -> rule8) triple6) -> rule6) OR ((((triple9) -> rule5) triple6) -> rule6))] The tiger visits the cow.[(((((triple2) -> rule7)) -> rule2) OR ((((triple9) -> rule7)) -> rule2))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow is red.
("cow" "is" "red" "+")
triple3
The cow needs the dog.
("cow" "needs" "dog" "+")
triple4
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple5
The dog needs the cow.
("dog" "needs" "cow" "+")
triple6
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple7
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple8
The tiger is cold.
("tiger" "is" "cold" "+")
triple9
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple10
The cow chases the dog.
("cow" "chases" "dog" "+")
((triple2) -> (rule5 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
((triple3) -> (rule8 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
((triple2) -> (rule7 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
((triple9) -> (rule5 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((triple8) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple9) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((((triple2) -> (rule5 % int2)) triple6) -> (rule6 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
((((triple3) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
((((triple9) -> (rule5 % int2)) triple6) -> (rule6 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
((((triple9) -> (rule7 % int2))) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2