The cow does not chase the tiger. The cow is rough. The cow needs the tiger. The cow sees the tiger. The tiger chases the cow. The tiger is big. The tiger is blue. The tiger is cold. The tiger is not rough. The tiger is young. The tiger needs the cow. The tiger sees the cow. If something needs the cow then the cow is not blue. If something is big then it chases the tiger.
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
The cow is rough.
("cow" "is" "rough" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the tiger.
("cow" "sees" "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 is cold.
("tiger" "is" "cold" "+")
The tiger is not 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 something needs the cow then the cow is not blue.
((("something" "needs" "cow" "+")) -> ("cow" "is" "blue" "-"))
If something is big then it chases the tiger.
((("something" "is" "big" "+")) -> ("something" "chases" "tiger" "+"))
The tiger chases the cow.
True
1
proof
[(triple5)]
("tiger" "chases" "cow" "+")
triple5
The cow is not rough.
False
1
inv-proof
[(triple2)]
("cow" "is" "rough" "-")
triple2
The cow is not blue.
True
2
proof
[(((triple11) -> rule1))]
("cow" "is" "blue" "-")
((triple11) -> (rule1 % int1))
The cow is not blue.
("cow" "is" "blue" "-")
int1
The tiger does not chase the tiger.
False
2
inv-proof
[(((triple6) -> rule2))]
("tiger" "chases" "tiger" "-")
((triple6) -> (rule2 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
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 cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
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 tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The cow does not chase the tiger.[(triple1)] The cow is rough.[(triple2)] The cow needs the tiger.[(triple3)] The cow sees the tiger.[(triple4)] The tiger chases the cow.[(triple5)] The tiger is big.[(triple6)] The tiger is blue.[(triple7)] The tiger is cold.[(triple8)] The tiger is not rough.[(triple9)] The tiger is young.[(triple10)] The tiger needs the cow.[(triple11)] The tiger sees the cow.[(triple12)] @1: The cow is not blue.[(((triple11) -> rule1))] The tiger chases the tiger.[(((triple6) -> rule2))]
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
triple1
The cow is rough.
("cow" "is" "rough" "+")
triple2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple3
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple4
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple5
The tiger is big.
("tiger" "is" "big" "+")
triple6
The tiger is blue.
("tiger" "is" "blue" "+")
triple7
The tiger is cold.
("tiger" "is" "cold" "+")
triple8
The tiger is not rough.
("tiger" "is" "rough" "-")
triple9
The tiger is young.
("tiger" "is" "young" "+")
triple10
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple11
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple12
The cow is not blue.
("cow" "is" "blue" "-")
((triple11) -> (rule1 % int1))
The cow is not blue.
("cow" "is" "blue" "-")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple6) -> (rule2 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1