The cow chases the tiger. The tiger visits the cow. If someone chases the tiger and the tiger chases the cow then the cow chases the tiger. If someone chases the cow and the cow chases the tiger then the cow eats the tiger. If someone chases the tiger and they visit the cow then the cow eats the tiger. If the cow eats the tiger then the tiger is not cold. If the tiger does not eat the cow and the tiger does not chase the cow then the tiger is young. If someone chases the cow and the cow eats the tiger then the tiger is young. If someone visits the cow then they chase the tiger. If the tiger is young then the tiger visits the cow.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If someone chases the tiger and the tiger chases the cow then the cow chases the tiger.
((("someone" "chases" "tiger" "+") ("tiger" "chases" "cow" "+")) -> ("cow" "chases" "tiger" "+"))
If someone chases the cow and the cow chases the tiger then the cow eats the tiger.
((("someone" "chases" "cow" "+") ("cow" "chases" "tiger" "+")) -> ("cow" "eats" "tiger" "+"))
If someone chases the tiger and they visit the cow then the cow eats the tiger.
((("someone" "chases" "tiger" "+") ("someone" "visits" "cow" "+")) -> ("cow" "eats" "tiger" "+"))
If the cow eats the tiger then the tiger is not cold.
((("cow" "eats" "tiger" "+")) -> ("tiger" "is" "cold" "-"))
If the tiger does not eat the cow and the tiger does not chase the cow then the tiger is young.
((("tiger" "eats" "cow" "~") ("tiger" "chases" "cow" "~")) -> ("tiger" "is" "young" "+"))
If someone chases the cow and the cow eats the tiger then the tiger is young.
((("someone" "chases" "cow" "+") ("cow" "eats" "tiger" "+")) -> ("tiger" "is" "young" "+"))
If someone visits the cow then they chase the tiger.
((("someone" "visits" "cow" "+")) -> ("someone" "chases" "tiger" "+"))
If the tiger is young then the tiger visits the cow.
((("tiger" "is" "young" "+")) -> ("tiger" "visits" "cow" "+"))
The cow chases the tiger.
True
1
proof
[(triple1)]
("cow" "chases" "tiger" "+")
triple1
The cow does not chase the tiger.
False
1
inv-proof
[(triple1)]
("cow" "chases" "tiger" "-")
triple1
The tiger chases the tiger.
True
2
proof
[(((triple2) -> rule7))]
("tiger" "chases" "tiger" "+")
((triple2) -> (rule7 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger does not chase the tiger.
False
2
inv-proof
[(((triple2) -> rule7))]
("tiger" "chases" "tiger" "-")
((triple2) -> (rule7 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The cow eats the tiger.
True
4
proof
[(((((triple2) -> rule7) triple2) -> rule3))]
("cow" "eats" "tiger" "+")
((((triple2) -> (rule7 % int2)) triple2) -> (rule3 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The cow does not eat the tiger.
False
4
inv-proof
[(((((triple2) -> rule7) triple2) -> rule3))]
("cow" "eats" "tiger" "-")
((((triple2) -> (rule7 % int2)) triple2) -> (rule3 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger is not cold.
True
5
proof
[(((((((triple2) -> rule7) triple2) -> rule3)) -> rule4))]
("tiger" "is" "cold" "-")
((((((triple2) -> (rule7 % int3)) triple2) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3
The tiger is cold.
False
5
inv-proof
[(((((((triple2) -> rule7) triple2) -> rule3)) -> rule4))]
("tiger" "is" "cold" "+")
((((((triple2) -> (rule7 % int3)) triple2) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "young" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
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 cow.
Unknown
random
[@0: The tiger eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "cow" "+")
@0: The cow chases the tiger.[(triple1)] The tiger visits the cow.[(triple2)] @1: The tiger chases the tiger.[(((triple2) -> rule7))] @2: The cow eats the tiger.[(((((triple2) -> rule7) triple2) -> rule3))] @3: The tiger is not cold.[(((((((triple2) -> rule7) triple2) -> rule3)) -> rule4))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple2) -> (rule7 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
((((triple2) -> (rule7 % int2)) triple2) -> (rule3 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger is not cold.
("tiger" "is" "cold" "-")
((((((triple2) -> (rule7 % int3)) triple2) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3