The bear is cold. The cow chases the bear. The cow eats the bear. The cow eats the lion. The cow is round. The cow visits the rabbit. The lion chases the cow. The lion is green. The rabbit eats the bear. The rabbit is round. If someone eats the bear and they visit the rabbit then the rabbit does not chase the lion. If someone visits the bear then the bear visits the rabbit. If someone chases the bear then they visit the lion. If someone is round then they are cold. If someone is cold then they do not visit the cow. If someone is round and they do not visit the cow then they chase the cow.
The bear is cold.
("bear" "is" "cold" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is round.
("cow" "is" "round" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion is green.
("lion" "is" "green" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
If someone eats the bear and they visit the rabbit then the rabbit does not chase the lion.
((("someone" "eats" "bear" "+") ("someone" "visits" "rabbit" "+")) -> ("rabbit" "chases" "lion" "-"))
If someone visits the bear then the bear visits the rabbit.
((("someone" "visits" "bear" "+")) -> ("bear" "visits" "rabbit" "+"))
If someone chases the bear then they visit the lion.
((("someone" "chases" "bear" "+")) -> ("someone" "visits" "lion" "+"))
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold then they do not visit the cow.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "cow" "-"))
If someone is round and they do not visit the cow then they chase the cow.
((("someone" "is" "round" "+") ("someone" "visits" "cow" "~")) -> ("someone" "chases" "cow" "+"))
The lion chases the cow.
True
1
proof
[(triple7)]
("lion" "chases" "cow" "+")
triple7
The lion is not green.
False
1
inv-proof
[(triple8)]
("lion" "is" "green" "-")
triple8
The cow is cold.
True
2
proof
[(((triple5) -> rule4))]
("cow" "is" "cold" "+")
((triple5) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is not cold.
False
2
inv-proof
[(((triple5) -> rule4))]
("cow" "is" "cold" "-")
((triple5) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow does not visit the cow.
True
3
proof
[(((((triple5) -> rule4)) -> rule5))]
("cow" "visits" "cow" "-")
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The cow does not visit the cow.
("cow" "visits" "cow" "-")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The rabbit visits the cow.
False
3
inv-proof
[(((((triple10) -> rule4)) -> rule5))]
("rabbit" "visits" "cow" "+")
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit does not visit the cow.
("rabbit" "visits" "cow" "-")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The cow chases the cow.
True
5
proof
[(((triple5 ((((triple5) -> rule4)) -> rule5)) -> rule6))]
("cow" "chases" "cow" "+")
((triple5 ((((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow does not visit the cow.
("cow" "visits" "cow" "-")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow does not chase the cow.
False
5
inv-proof
[(((triple5 ((((triple5) -> rule4)) -> rule5)) -> rule6))]
("cow" "chases" "cow" "-")
((triple5 ((((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow does not visit the cow.
("cow" "visits" "cow" "-")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The bear does not visit the lion.
Unknown
inv-rconc
[@1: The bear visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "visits" "lion" "-")
The bear visits the rabbit.
Unknown
rconc
[@1: The bear visits the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "visits" "rabbit" "+")
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "cold" "-")
The rabbit visits the lion.
Unknown
rconc
[@1: The rabbit visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "visits" "lion" "+")
The lion does not chase the rabbit.
Unknown
inv-random
[@0: The lion chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "rabbit" "-")
The lion chases the bear.
Unknown
random
[@0: The lion chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "bear" "+")
The rabbit does not visit the bear.
Unknown
inv-random
[@0: The rabbit visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "bear" "-")
The bear chases the rabbit.
Unknown
random
[@0: The bear chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "rabbit" "+")
@0: The bear is cold.[(triple1)] The cow chases the bear.[(triple2)] The cow eats the bear.[(triple3)] The cow eats the lion.[(triple4)] The cow is round.[(triple5)] The cow visits the rabbit.[(triple6)] The lion chases the cow.[(triple7)] The lion is green.[(triple8)] The rabbit eats the bear.[(triple9)] The rabbit is round.[(triple10)] @1: The bear does not visit the cow.[(((triple1) -> rule5))] The cow is cold.[(((triple5) -> rule4))] The cow visits the lion.[(((triple2) -> rule3))] The rabbit does not chase the lion.[(((triple3 triple6) -> rule1))] The rabbit is cold.[(((triple10) -> rule4))] @2: The cow does not visit the cow.[(((((triple5) -> rule4)) -> rule5))] The rabbit does not visit the cow.[(((((triple10) -> rule4)) -> rule5))] @3: The cow chases the cow.[(((triple5 ((((triple5) -> rule4)) -> rule5)) -> rule6))] The rabbit chases the cow.[(((triple10 ((((triple10) -> rule4)) -> rule5)) -> rule6))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The cow chases the bear.
("cow" "chases" "bear" "+")
triple2
The cow eats the bear.
("cow" "eats" "bear" "+")
triple3
The cow eats the lion.
("cow" "eats" "lion" "+")
triple4
The cow is round.
("cow" "is" "round" "+")
triple5
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple6
The lion chases the cow.
("lion" "chases" "cow" "+")
triple7
The lion is green.
("lion" "is" "green" "+")
triple8
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple9
The rabbit is round.
("rabbit" "is" "round" "+")
triple10
The bear does not visit the cow.
("bear" "visits" "cow" "-")
((triple1) -> (rule5 % int1))
The bear does not visit the cow.
("bear" "visits" "cow" "-")
int1
The cow is cold.
("cow" "is" "cold" "+")
((triple5) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
((triple2) -> (rule3 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
((triple3 triple6) -> (rule1 % int1))
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple10) -> (rule4 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The cow does not visit the cow.
("cow" "visits" "cow" "-")
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The cow does not visit the cow.
("cow" "visits" "cow" "-")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The rabbit does not visit the cow.
("rabbit" "visits" "cow" "-")
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit does not visit the cow.
("rabbit" "visits" "cow" "-")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple5 ((((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow does not visit the cow.
("cow" "visits" "cow" "-")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
((triple10 ((((triple10) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit does not visit the cow.
("rabbit" "visits" "cow" "-")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3