The cow chases the tiger. The cow is cold. The cow is not red. The cow visits the tiger. The tiger is big. The tiger is red. The tiger is not round. If the cow is cold then the cow is round. If the cow chases the tiger then the cow is not nice. If something likes the cow and it visits the cow then it likes the tiger. If something chases the cow then it does not like the cow. If something chases the tiger and it likes the cow then it is red. If something likes the tiger and the tiger is not nice then the tiger chases the cow. If the tiger does not visit the cow then the cow likes the tiger. If something chases the cow and the cow likes the tiger then it chases the tiger.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is not red.
("cow" "is" "red" "-")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is not round.
("tiger" "is" "round" "-")
If the cow is cold then the cow is round.
((("cow" "is" "cold" "+")) -> ("cow" "is" "round" "+"))
If the cow chases the tiger then the cow is not nice.
((("cow" "chases" "tiger" "+")) -> ("cow" "is" "nice" "-"))
If something likes the cow and it visits the cow then it likes the tiger.
((("something" "likes" "cow" "+") ("something" "visits" "cow" "+")) -> ("something" "likes" "tiger" "+"))
If something chases the cow then it does not like the cow.
((("something" "chases" "cow" "+")) -> ("something" "likes" "cow" "-"))
If something chases the tiger and it likes the cow then it is red.
((("something" "chases" "tiger" "+") ("something" "likes" "cow" "+")) -> ("something" "is" "red" "+"))
If something likes the tiger and the tiger is not nice then the tiger chases the cow.
((("something" "likes" "tiger" "+") ("tiger" "is" "nice" "~")) -> ("tiger" "chases" "cow" "+"))
If the tiger does not visit the cow then the cow likes the tiger.
((("tiger" "visits" "cow" "~")) -> ("cow" "likes" "tiger" "+"))
If something chases the cow and the cow likes the tiger then it chases the tiger.
((("something" "chases" "cow" "+") ("cow" "likes" "tiger" "+")) -> ("something" "chases" "tiger" "+"))
The tiger is big.
True
1
proof
[(triple5)]
("tiger" "is" "big" "+")
triple5
The cow does not visit the tiger.
False
1
inv-proof
[(triple4)]
("cow" "visits" "tiger" "-")
triple4
The cow is round.
True
2
proof
[(((triple2) -> rule1))]
("cow" "is" "round" "+")
((triple2) -> (rule1 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is not round.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "is" "round" "-")
((triple2) -> (rule1 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The tiger does not chase the tiger.
Unknown
inv-rconc
[@2: The tiger chases the tiger.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The cow likes the tiger.
Unknown
rconc
[@1: The cow likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "likes" "tiger" "+")
The tiger does not visit the cow.
Unknown
inv-random
[@0: The tiger visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "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 cold.[(triple2)] The cow is not red.[(triple3)] The cow visits the tiger.[(triple4)] The tiger is big.[(triple5)] The tiger is not round.[(triple7)] The tiger is red.[(triple6)] @1: The cow is not nice.[(((triple1) -> rule2))] The cow is round.[(((triple2) -> rule1))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow is not red.
("cow" "is" "red" "-")
triple3
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple4
The tiger is big.
("tiger" "is" "big" "+")
triple5
The tiger is not round.
("tiger" "is" "round" "-")
triple7
The tiger is red.
("tiger" "is" "red" "+")
triple6
The cow is not nice.
("cow" "is" "nice" "-")
((triple1) -> (rule2 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is round.
("cow" "is" "round" "+")
((triple2) -> (rule1 % int1))
The cow is round.
("cow" "is" "round" "+")
int1