The bear chases the squirrel. The bear chases the tiger. The bear is not cold. The bear visits the tiger. The cow does not chase the squirrel. The cow is cold. The cow likes the bear. The squirrel chases the bear. The tiger chases the squirrel. The tiger is red. If something likes the squirrel then it is cold. If the tiger likes the cow and the tiger is red then the cow does not visit the bear. If something is kind and it does not chase the tiger then the tiger is kind. If something visits the cow then it is big. If something is red then it visits the cow. If something chases the bear and it is not red then the bear likes the cow.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is not cold.
("bear" "is" "cold" "-")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The cow does not chase the squirrel.
("cow" "chases" "squirrel" "-")
The cow is cold.
("cow" "is" "cold" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger is red.
("tiger" "is" "red" "+")
If something likes the squirrel then it is cold.
((("something" "likes" "squirrel" "+")) -> ("something" "is" "cold" "+"))
If the tiger likes the cow and the tiger is red then the cow does not visit the bear.
((("tiger" "likes" "cow" "+") ("tiger" "is" "red" "+")) -> ("cow" "visits" "bear" "-"))
If something is kind and it does not chase the tiger then the tiger is kind.
((("something" "is" "kind" "+") ("something" "chases" "tiger" "~")) -> ("tiger" "is" "kind" "+"))
If something visits the cow then it is big.
((("something" "visits" "cow" "+")) -> ("something" "is" "big" "+"))
If something is red then it visits the cow.
((("something" "is" "red" "+")) -> ("something" "visits" "cow" "+"))
If something chases the bear and it is not red then the bear likes the cow.
((("something" "chases" "bear" "+") ("something" "is" "red" "~")) -> ("bear" "likes" "cow" "+"))
The cow does not chase the squirrel.
True
1
proof
[(triple5)]
("cow" "chases" "squirrel" "-")
triple5
The bear does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("bear" "chases" "squirrel" "-")
triple1
The tiger visits the cow.
True
2
proof
[(((triple10) -> rule5))]
("tiger" "visits" "cow" "+")
((triple10) -> (rule5 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger does not visit the cow.
False
2
inv-proof
[(((triple10) -> rule5))]
("tiger" "visits" "cow" "-")
((triple10) -> (rule5 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger is big.
True
3
proof
[(((((triple10) -> rule5)) -> rule4))]
("tiger" "is" "big" "+")
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The tiger is not big.
False
3
inv-proof
[(((((triple10) -> rule5)) -> rule4))]
("tiger" "is" "big" "-")
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The squirrel is not big.
Unknown
inv-rconc
[@2: The squirrel is big.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("squirrel" "is" "big" "-")
The cow visits the cow.
Unknown
rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "visits" "cow" "+")
The bear is not big.
Unknown
inv-rconc
[@2: The bear is big.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("bear" "is" "big" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The cow does not like the tiger.
Unknown
inv-random
[@0: The cow likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "tiger" "-")
The tiger chases the bear.
Unknown
random
[@0: The tiger chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "bear" "+")
@0: The bear chases the squirrel.[(triple1)] The bear chases the tiger.[(triple2)] The bear is not cold.[(triple3)] The bear visits the tiger.[(triple4)] The cow does not chase the squirrel.[(triple5)] The cow is cold.[(triple6)] The cow likes the bear.[(triple7)] The squirrel chases the bear.[(triple8)] The tiger chases the squirrel.[(triple9)] The tiger is red.[(triple10)] @1: The tiger visits the cow.[(((triple10) -> rule5))] @2: The tiger is big.[(((((triple10) -> rule5)) -> rule4))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple2
The bear is not cold.
("bear" "is" "cold" "-")
triple3
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple4
The cow does not chase the squirrel.
("cow" "chases" "squirrel" "-")
triple5
The cow is cold.
("cow" "is" "cold" "+")
triple6
The cow likes the bear.
("cow" "likes" "bear" "+")
triple7
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple8
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple9
The tiger is red.
("tiger" "is" "red" "+")
triple10
The tiger visits the cow.
("tiger" "visits" "cow" "+")
((triple10) -> (rule5 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2