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