The cow does not chase the tiger. The cow is not big. The cow is red. The cow is rough. The cow needs the dog. The dog chases the tiger. The dog is cold. The tiger chases the cow. The tiger eats the cow. The tiger needs the cow. If something is red and it chases the dog then it needs the cow. If something is kind then it chases the cow. If something chases the cow and it is not big then it does not eat the dog. If something chases the cow then the cow chases the dog. If something needs the tiger then the tiger is cold. If something eats the tiger and the tiger does not eat the cow then the tiger is not cold. If something is rough and it needs the cow then the cow eats the dog. If something eats the tiger and it is big then it is red.
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
The cow is not big.
("cow" "is" "big" "-")
The cow is red.
("cow" "is" "red" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is cold.
("dog" "is" "cold" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
If something is red and it chases the dog then it needs the cow.
((("something" "is" "red" "+") ("something" "chases" "dog" "+")) -> ("something" "needs" "cow" "+"))
If something is kind then it chases the cow.
((("something" "is" "kind" "+")) -> ("something" "chases" "cow" "+"))
If something chases the cow and it is not big then it does not eat the dog.
((("something" "chases" "cow" "+") ("something" "is" "big" "~")) -> ("something" "eats" "dog" "-"))
If something chases the cow then the cow chases the dog.
((("something" "chases" "cow" "+")) -> ("cow" "chases" "dog" "+"))
If something needs the tiger then the tiger is cold.
((("something" "needs" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
If something eats the tiger and the tiger does not eat the cow then the tiger is not cold.
((("something" "eats" "tiger" "+") ("tiger" "eats" "cow" "~")) -> ("tiger" "is" "cold" "-"))
If something is rough and it needs the cow then the cow eats the dog.
((("something" "is" "rough" "+") ("something" "needs" "cow" "+")) -> ("cow" "eats" "dog" "+"))
If something eats the tiger and it is big then it is red.
((("something" "eats" "tiger" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
The cow is red.
True
1
proof
[(triple3)]
("cow" "is" "red" "+")
triple3
The cow chases the tiger.
False
1
inv-proof
[(triple1)]
("cow" "chases" "tiger" "+")
triple1
The cow chases the dog.
True
2
proof
[(((triple8) -> rule4))]
("cow" "chases" "dog" "+")
((triple8) -> (rule4 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow does not chase the dog.
False
2
inv-proof
[(((triple8) -> rule4))]
("cow" "chases" "dog" "-")
((triple8) -> (rule4 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow needs the cow.
True
4
proof
[(((triple3 ((triple8) -> rule4)) -> rule1))]
("cow" "needs" "cow" "+")
((triple3 ((triple8) -> (rule4 % int2))) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
The cow does not need the cow.
False
4
inv-proof
[(((triple3 ((triple8) -> rule4)) -> rule1))]
("cow" "needs" "cow" "-")
((triple3 ((triple8) -> (rule4 % int2))) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
The cow eats the dog.
True
6
proof
[(((triple4 ((triple3 ((triple8) -> rule4)) -> rule1)) -> rule7))]
("cow" "eats" "dog" "+")
((triple4 ((triple3 ((triple8) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
int3
The cow does not eat the dog.
False
6
inv-proof
[(((triple4 ((triple3 ((triple8) -> rule4)) -> rule1)) -> rule7))]
("cow" "eats" "dog" "-")
((triple4 ((triple3 ((triple8) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
int3
The dog is not red.
Unknown
inv-rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "is" "red" "-")
The tiger is red.
Unknown
rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "is" "red" "+")
The tiger is not cold.
Unknown
inv-rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "cold" "-")
The dog chases the cow.
Unknown
rconc
[@1: The dog chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "cow" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
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 rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The cow does not chase the tiger.[(triple1)] The cow is not big.[(triple2)] The cow is red.[(triple3)] The cow is rough.[(triple4)] The cow needs the dog.[(triple5)] The dog chases the tiger.[(triple6)] The dog is cold.[(triple7)] The tiger chases the cow.[(triple8)] The tiger eats the cow.[(triple9)] The tiger needs the cow.[(triple10)] @1: The cow chases the dog.[(((triple8) -> rule4))] @2: The cow needs the cow.[(((triple3 ((triple8) -> rule4)) -> rule1))] @3: The cow eats the dog.[(((triple4 ((triple3 ((triple8) -> rule4)) -> rule1)) -> rule7))]
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
triple1
The cow is not big.
("cow" "is" "big" "-")
triple2
The cow is red.
("cow" "is" "red" "+")
triple3
The cow is rough.
("cow" "is" "rough" "+")
triple4
The cow needs the dog.
("cow" "needs" "dog" "+")
triple5
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple6
The dog is cold.
("dog" "is" "cold" "+")
triple7
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple8
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple9
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple10
The cow chases the dog.
("cow" "chases" "dog" "+")
((triple8) -> (rule4 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple3 ((triple8) -> (rule4 % int2))) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
The cow eats the dog.
("cow" "eats" "dog" "+")
((triple4 ((triple3 ((triple8) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
int3