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