The cow chases the tiger. The cow is blue. The cow is nice. The cow likes the tiger. The cow visits the tiger. The tiger chases the cow. The tiger is blue. The tiger is nice. The tiger likes the cow. The tiger visits the cow. If someone chases the tiger and the tiger is nice then the tiger is cold.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If someone chases the tiger and the tiger is nice then the tiger is cold.
((("someone" "chases" "tiger" "+") ("tiger" "is" "nice" "+")) -> ("tiger" "is" "cold" "+"))
The tiger is blue.
True
1
proof
[(triple7)]
("tiger" "is" "blue" "+")
triple7
The tiger does not like the cow.
False
1
inv-proof
[(triple9)]
("tiger" "likes" "cow" "-")
triple9
The tiger is cold.
True
3
proof
[(((triple1 triple8) -> rule1))]
("tiger" "is" "cold" "+")
((triple1 triple8) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not cold.
False
3
inv-proof
[(((triple1 triple8) -> rule1))]
("tiger" "is" "cold" "-")
((triple1 triple8) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The cow chases the tiger.[(triple1)] The cow is blue.[(triple2)] The cow is nice.[(triple3)] The cow likes the tiger.[(triple4)] The cow visits the tiger.[(triple5)] The tiger chases the cow.[(triple6)] The tiger is blue.[(triple7)] The tiger is nice.[(triple8)] The tiger likes the cow.[(triple9)] The tiger visits the cow.[(triple10)] @1: The tiger is cold.[(((triple1 triple8) -> rule1))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple4
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple5
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple6
The tiger is blue.
("tiger" "is" "blue" "+")
triple7
The tiger is nice.
("tiger" "is" "nice" "+")
triple8
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple9
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
((triple1 triple8) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1