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