The cow eats the tiger. The cow is big. The cow is green. The cow is rough. The cow is young. The cow needs the tiger. The cow sees the tiger. The tiger eats the cow. The tiger is big. The tiger is cold. The tiger is green. The tiger is rough. The tiger is young. The tiger needs the cow. The tiger sees the cow. If someone needs the cow and the cow is big then they see the cow. If the tiger is young and the tiger eats the cow then the cow is cold. If someone sees the cow and they see the tiger then the cow is young. If someone eats the tiger and the tiger eats the cow then the tiger is cold. If someone eats the cow and the cow is young then the cow is big. If someone is rough and they see the tiger then they need the tiger. If someone sees the cow then they are green. If someone is cold then they are green.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If someone needs the cow and the cow is big then they see the cow.
((("someone" "needs" "cow" "+") ("cow" "is" "big" "+")) -> ("someone" "sees" "cow" "+"))
If the tiger is young and the tiger eats the cow then the cow is cold.
((("tiger" "is" "young" "+") ("tiger" "eats" "cow" "+")) -> ("cow" "is" "cold" "+"))
If someone sees the cow and they see the tiger then the cow is young.
((("someone" "sees" "cow" "+") ("someone" "sees" "tiger" "+")) -> ("cow" "is" "young" "+"))
If someone eats the tiger and the tiger eats the cow then the tiger is cold.
((("someone" "eats" "tiger" "+") ("tiger" "eats" "cow" "+")) -> ("tiger" "is" "cold" "+"))
If someone eats the cow and the cow is young then the cow is big.
((("someone" "eats" "cow" "+") ("cow" "is" "young" "+")) -> ("cow" "is" "big" "+"))
If someone is rough and they see the tiger then they need the tiger.
((("someone" "is" "rough" "+") ("someone" "sees" "tiger" "+")) -> ("someone" "needs" "tiger" "+"))
If someone sees the cow then they are green.
((("someone" "sees" "cow" "+")) -> ("someone" "is" "green" "+"))
If someone is cold then they are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
The cow is young.
True
1
proof
[(triple5)]
("cow" "is" "young" "+")
triple5
The cow does not eat the tiger.
False
1
inv-proof
[(triple1)]
("cow" "eats" "tiger" "-")
triple1
The cow is cold.
True
3
proof
[(((triple13 triple8) -> rule2))]
("cow" "is" "cold" "+")
((triple13 triple8) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is not cold.
False
3
inv-proof
[(((triple13 triple8) -> rule2))]
("cow" "is" "cold" "-")
((triple13 triple8) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The cow sees the cow.
Unknown
rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "cow" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow eats the tiger.[(triple1)] The cow is big.[(triple2 OR ((triple8 triple5) -> rule5))] The cow is green.[(triple3 OR ((((triple13 triple8) -> rule2)) -> rule8))] The cow is rough.[(triple4)] The cow is young.[(triple5)] The cow needs the tiger.[(triple6 OR ((triple4 triple7) -> rule6))] The cow sees the tiger.[(triple7)] The tiger eats the cow.[(triple8)] The tiger is big.[(triple9)] The tiger is cold.[(triple10 OR ((triple1 triple8) -> rule4))] The tiger is green.[(triple11 OR ((triple10) -> rule8) OR ((triple15) -> rule7) OR ((((triple1 triple8) -> rule4)) -> rule8) OR ((((triple14 triple2) -> rule1)) -> rule7) OR ((((triple14 ((triple8 triple5) -> rule5)) -> rule1)) -> rule7))] The tiger is rough.[(triple12)] The tiger is young.[(triple13)] The tiger needs the cow.[(triple14)] The tiger sees the cow.[(triple15 OR ((triple14 triple2) -> rule1) OR ((triple14 ((triple8 triple5) -> rule5)) -> rule1))] @1: The cow is cold.[(((triple13 triple8) -> rule2))]
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
((triple8 triple5) -> (rule5 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is green.
("cow" "is" "green" "+")
triple3
((((triple13 triple8) -> (rule2 % int2))) -> (rule8 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple6
((triple4 triple7) -> (rule6 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple7
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
((triple1 triple8) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
triple11
((triple10) -> (rule8 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((triple15) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((((triple1 triple8) -> (rule4 % int2))) -> (rule8 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
((((triple14 triple2) -> (rule1 % int2))) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
((((triple14 ((triple8 triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple14
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple15
((triple14 triple2) -> (rule1 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
((triple14 ((triple8 triple5) -> (rule5 % int2))) -> (rule1 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
((triple13 triple8) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1