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