The cow chases the lion. The cow eats the lion. The cow is nice. The cow is red. The cow is rough. The cow sees the lion. The lion chases the cow. The lion is red. The lion is not round. The lion sees the cow. All cold, rough things are round. If something is cold then it chases the lion. If the lion sees the cow and the lion chases the cow then the cow sees the lion. If something is round and not nice then it is rough. If the cow chases the lion and the lion sees the cow then the lion is cold. If the lion is rough then the lion sees the cow. If something is cold and it chases the lion then it eats the cow. If the lion eats the cow and the cow does not see the lion then the lion is red.
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is not round.
("lion" "is" "round" "-")
The lion sees the cow.
("lion" "sees" "cow" "+")
All cold, rough things are round.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is cold then it chases the lion.
((("something" "is" "cold" "+")) -> ("something" "chases" "lion" "+"))
If the lion sees the cow and the lion chases the cow then the cow sees the lion.
((("lion" "sees" "cow" "+") ("lion" "chases" "cow" "+")) -> ("cow" "sees" "lion" "+"))
If something is round and not nice then it is rough.
((("something" "is" "round" "+") ("something" "is" "nice" "~")) -> ("something" "is" "rough" "+"))
If the cow chases the lion and the lion sees the cow then the lion is cold.
((("cow" "chases" "lion" "+") ("lion" "sees" "cow" "+")) -> ("lion" "is" "cold" "+"))
If the lion is rough then the lion sees the cow.
((("lion" "is" "rough" "+")) -> ("lion" "sees" "cow" "+"))
If something is cold and it chases the lion then it eats the cow.
((("something" "is" "cold" "+") ("something" "chases" "lion" "+")) -> ("something" "eats" "cow" "+"))
If the lion eats the cow and the cow does not see the lion then the lion is red.
((("lion" "eats" "cow" "+") ("cow" "sees" "lion" "~")) -> ("lion" "is" "red" "+"))
The cow is rough.
True
1
proof
[(triple5)]
("cow" "is" "rough" "+")
triple5
The lion does not chase the cow.
False
1
inv-proof
[(triple7)]
("lion" "chases" "cow" "-")
triple7
The lion is cold.
True
3
proof
[(((triple1 triple10) -> rule5))]
("lion" "is" "cold" "+")
((triple1 triple10) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is not cold.
False
3
inv-proof
[(((triple1 triple10) -> rule5))]
("lion" "is" "cold" "-")
((triple1 triple10) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion chases the lion.
True
4
proof
[(((((triple1 triple10) -> rule5)) -> rule2))]
("lion" "chases" "lion" "+")
((((triple1 triple10) -> (rule5 % int2))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion does not chase the lion.
False
4
inv-proof
[(((((triple1 triple10) -> rule5)) -> rule2))]
("lion" "chases" "lion" "-")
((((triple1 triple10) -> (rule5 % int2))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion eats the cow.
True
8
proof
[(((((triple1 triple10) -> rule5) ((((triple1 triple10) -> rule5)) -> rule2)) -> rule7))]
("lion" "eats" "cow" "+")
((((triple1 triple10) -> (rule5 % int3)) ((((triple1 triple10) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion does not eat the cow.
False
8
inv-proof
[(((((triple1 triple10) -> rule5) ((((triple1 triple10) -> rule5)) -> rule2)) -> rule7))]
("lion" "eats" "cow" "-")
((((triple1 triple10) -> (rule5 % int3)) ((((triple1 triple10) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "eats" "cow" "-")
The lion is rough.
Unknown
rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "rough" "+")
The cow is not round.
Unknown
inv-rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "round" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow chases the lion.[(triple1)] The cow eats the lion.[(triple2)] The cow is nice.[(triple3)] The cow is red.[(triple4)] The cow is rough.[(triple5)] The cow sees the lion.[(triple6 OR ((triple10 triple7) -> rule3))] The lion chases the cow.[(triple7)] The lion is not round.[(triple9)] The lion is red.[(triple8)] The lion sees the cow.[(triple10)] @1: The lion is cold.[(((triple1 triple10) -> rule5))] @2: The lion chases the lion.[(((((triple1 triple10) -> rule5)) -> rule2))] @3: The lion eats the cow.[(((((triple1 triple10) -> rule5) ((((triple1 triple10) -> rule5)) -> rule2)) -> rule7))]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
The cow eats the lion.
("cow" "eats" "lion" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow is rough.
("cow" "is" "rough" "+")
triple5
The cow sees the lion.
("cow" "sees" "lion" "+")
triple6
((triple10 triple7) -> (rule3 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
triple7
The lion is not round.
("lion" "is" "round" "-")
triple9
The lion is red.
("lion" "is" "red" "+")
triple8
The lion sees the cow.
("lion" "sees" "cow" "+")
triple10
The lion is cold.
("lion" "is" "cold" "+")
((triple1 triple10) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
((((triple1 triple10) -> (rule5 % int2))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion eats the cow.
("lion" "eats" "cow" "+")
((((triple1 triple10) -> (rule5 % int3)) ((((triple1 triple10) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3