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