The cow is big. The cow is cold. The cow is green. The cow is nice. The cow is round. The cow likes the tiger. The cow needs the tiger. The cow sees the tiger. The tiger is big. The tiger is cold. The tiger is green. The tiger is nice. The tiger is round. The tiger likes the cow. The tiger needs the cow. The tiger sees the cow. If the cow sees the tiger then the cow needs the tiger. If something likes the cow then it needs the tiger. If something is big then it sees the tiger. If something needs the tiger and it needs the cow then the cow likes the tiger. If something sees the tiger and the tiger needs the cow then the tiger sees the cow. If the tiger likes the cow then the cow sees the tiger. If something is nice and it sees the tiger then it sees the cow. If something likes the cow then it sees the cow.
The cow is big.
("cow" "is" "big" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is round.
("cow" "is" "round" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If the cow sees the tiger then the cow needs the tiger.
((("cow" "sees" "tiger" "+")) -> ("cow" "needs" "tiger" "+"))
If something likes the cow then it needs the tiger.
((("something" "likes" "cow" "+")) -> ("something" "needs" "tiger" "+"))
If something is big then it sees the tiger.
((("something" "is" "big" "+")) -> ("something" "sees" "tiger" "+"))
If something needs the tiger and it needs the cow then the cow likes the tiger.
((("something" "needs" "tiger" "+") ("something" "needs" "cow" "+")) -> ("cow" "likes" "tiger" "+"))
If something sees the tiger and the tiger needs the cow then the tiger sees the cow.
((("something" "sees" "tiger" "+") ("tiger" "needs" "cow" "+")) -> ("tiger" "sees" "cow" "+"))
If the tiger likes the cow then the cow sees the tiger.
((("tiger" "likes" "cow" "+")) -> ("cow" "sees" "tiger" "+"))
If something is nice and it sees the tiger then it sees the cow.
((("something" "is" "nice" "+") ("something" "sees" "tiger" "+")) -> ("something" "sees" "cow" "+"))
If something likes the cow then it sees the cow.
((("something" "likes" "cow" "+")) -> ("something" "sees" "cow" "+"))
The tiger is cold.
True
1
proof
[(triple10)]
("tiger" "is" "cold" "+")
triple10
The cow does not need the tiger.
False
1
inv-proof
[(triple7 OR ((triple8) -> rule1) OR ((((triple1) -> rule3)) -> rule1) OR ((((triple14) -> rule6)) -> rule1))]
("cow" "needs" "tiger" "-")
triple7
((triple8) -> (rule1 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
((((triple14) -> (rule6 % int2))) -> (rule1 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The tiger sees the tiger.
True
2
proof
[(((triple9) -> rule3))]
("tiger" "sees" "tiger" "+")
((triple9) -> (rule3 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The cow does not see the cow.
False
3
inv-proof
[(((triple4 triple8) -> rule7) OR ((triple4 ((triple1) -> rule3)) -> rule7) OR ((triple4 ((triple14) -> rule6)) -> rule7))]
("cow" "sees" "cow" "-")
((triple4 triple8) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
((triple4 ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
((triple4 ((triple14) -> (rule6 % int2))) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The cow is big.[(triple1)] The cow is cold.[(triple2)] The cow is green.[(triple3)] The cow is nice.[(triple4)] The cow is round.[(triple5)] The cow likes the tiger.[(triple6 OR ((((triple14) -> rule2) triple15) -> rule4))] The cow needs the tiger.[(triple7 OR ((triple8) -> rule1) OR ((((triple1) -> rule3)) -> rule1) OR ((((triple14) -> rule6)) -> rule1))] The cow sees the tiger.[(triple8 OR ((triple1) -> rule3) OR ((triple14) -> rule6))] The tiger is big.[(triple9)] The tiger is cold.[(triple10)] The tiger is green.[(triple11)] The tiger is nice.[(triple12)] The tiger is round.[(triple13)] The tiger likes the cow.[(triple14)] The tiger needs the cow.[(triple15)] The tiger sees the cow.[(triple16 OR ((triple14) -> rule8) OR ((triple8 triple15) -> rule5) OR ((triple12 ((triple9) -> rule3)) -> rule7) OR ((((triple1) -> rule3) triple15) -> rule5) OR ((((triple14) -> rule6) triple15) -> rule5) OR ((((triple9) -> rule3) triple15) -> rule5))] @1: The cow sees the cow.[(((triple4 triple8) -> rule7) OR ((triple4 ((triple1) -> rule3)) -> rule7) OR ((triple4 ((triple14) -> rule6)) -> rule7))] The tiger needs the tiger.[(((triple14) -> rule2))] The tiger sees the tiger.[(((triple9) -> rule3))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow is round.
("cow" "is" "round" "+")
triple5
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple6
((((triple14) -> (rule2 % int2)) triple15) -> (rule4 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple7
((triple8) -> (rule1 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
((((triple14) -> (rule6 % int2))) -> (rule1 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple8
((triple1) -> (rule3 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
((triple14) -> (rule6 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
The tiger is green.
("tiger" "is" "green" "+")
triple11
The tiger is nice.
("tiger" "is" "nice" "+")
triple12
The tiger is round.
("tiger" "is" "round" "+")
triple13
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple14
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple15
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple16
((triple14) -> (rule8 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
((triple8 triple15) -> (rule5 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
((triple12 ((triple9) -> (rule3 % int2))) -> (rule7 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
((((triple1) -> (rule3 % int2)) triple15) -> (rule5 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
((((triple14) -> (rule6 % int2)) triple15) -> (rule5 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
((((triple9) -> (rule3 % int2)) triple15) -> (rule5 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple4 triple8) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
((triple4 ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
((triple4 ((triple14) -> (rule6 % int2))) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple14) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple9) -> (rule3 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1