The bear does not like the cow. The cow chases the bear. The cow eats the bear. The cow is big. The cow is red. The cow is young. The cow likes the bear. If the cow chases the bear then the cow eats the bear. Cold things are young. All big things are young. If something chases the bear and the bear likes the cow then the bear does not eat the cow. If something is young and it does not like the cow then it is red. If something likes the cow then the cow is cold. If something eats the bear then the bear is big. If something chases the bear then it is round.
The bear does not like the cow.
("bear" "likes" "cow" "-")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
If the cow chases the bear then the cow eats the bear.
((("cow" "chases" "bear" "+")) -> ("cow" "eats" "bear" "+"))
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
All big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something chases the bear and the bear likes the cow then the bear does not eat the cow.
((("something" "chases" "bear" "+") ("bear" "likes" "cow" "+")) -> ("bear" "eats" "cow" "-"))
If something is young and it does not like the cow then it is red.
((("something" "is" "young" "+") ("something" "likes" "cow" "~")) -> ("something" "is" "red" "+"))
If something likes the cow then the cow is cold.
((("something" "likes" "cow" "+")) -> ("cow" "is" "cold" "+"))
If something eats the bear then the bear is big.
((("something" "eats" "bear" "+")) -> ("bear" "is" "big" "+"))
If something chases the bear then it is round.
((("something" "chases" "bear" "+")) -> ("something" "is" "round" "+"))
The bear does not like the cow.
True
1
proof
[(triple1)]
("bear" "likes" "cow" "-")
triple1
The cow does not chase the bear.
False
1
inv-proof
[(triple2)]
("cow" "chases" "bear" "-")
triple2
The cow is round.
True
2
proof
[(((triple2) -> rule8))]
("cow" "is" "round" "+")
((triple2) -> (rule8 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is not round.
False
2
inv-proof
[(((triple2) -> rule8))]
("cow" "is" "round" "-")
((triple2) -> (rule8 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The bear is young.
True
3
proof
[(((((triple3) -> rule7)) -> rule3) OR ((((((triple2) -> rule1)) -> rule7)) -> rule3))]
("bear" "is" "young" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The cow eats the bear.
("cow" "eats" "bear" "+")
int3
The bear is not young.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule3) OR ((((((triple2) -> rule1)) -> rule7)) -> rule3))]
("bear" "is" "young" "-")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The cow eats the bear.
("cow" "eats" "bear" "+")
int3
The bear is red.
True
5
proof
[(((((((triple3) -> rule7)) -> rule3) triple1) -> rule5) OR ((((((((triple2) -> rule1)) -> rule7)) -> rule3) triple1) -> rule5))]
("bear" "is" "red" "+")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2)) triple1) -> (rule5 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule3 % int2)) triple1) -> (rule5 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
The cow eats the bear.
("cow" "eats" "bear" "+")
int4
The bear is not red.
False
5
inv-proof
[(((((((triple3) -> rule7)) -> rule3) triple1) -> rule5) OR ((((((((triple2) -> rule1)) -> rule7)) -> rule3) triple1) -> rule5))]
("bear" "is" "red" "-")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2)) triple1) -> (rule5 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule3 % int2)) triple1) -> (rule5 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
The cow eats the bear.
("cow" "eats" "bear" "+")
int4
The cow is not cold.
Unknown
inv-rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "cold" "-")
The bear is round.
Unknown
rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "is" "round" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The bear eats the cow.
Unknown
random
[@0: The bear eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "cow" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The bear chases the cow.
Unknown
random
[@0: The bear chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "cow" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The bear does not like the cow.[(triple1)] The cow chases the bear.[(triple2)] The cow eats the bear.[(triple3 OR ((triple2) -> rule1))] The cow is big.[(triple4)] The cow is red.[(triple5)] The cow is young.[(triple6 OR ((triple4) -> rule3))] The cow likes the bear.[(triple7)] @1: The bear is big.[(((triple3) -> rule7) OR ((((triple2) -> rule1)) -> rule7))] The cow is round.[(((triple2) -> rule8))] @2: The bear is young.[(((((triple3) -> rule7)) -> rule3) OR ((((((triple2) -> rule1)) -> rule7)) -> rule3))] @3: The bear is red.[(((((((triple3) -> rule7)) -> rule3) triple1) -> rule5) OR ((((((((triple2) -> rule1)) -> rule7)) -> rule3) triple1) -> rule5))]
The bear does not like the cow.
("bear" "likes" "cow" "-")
triple1
The cow chases the bear.
("cow" "chases" "bear" "+")
triple2
The cow eats the bear.
("cow" "eats" "bear" "+")
triple3
((triple2) -> (rule1 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The cow is big.
("cow" "is" "big" "+")
triple4
The cow is red.
("cow" "is" "red" "+")
triple5
The cow is young.
("cow" "is" "young" "+")
triple6
((triple4) -> (rule3 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
triple7
The bear is big.
("bear" "is" "big" "+")
((triple3) -> (rule7 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The cow is round.
("cow" "is" "round" "+")
((triple2) -> (rule8 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The bear is young.
("bear" "is" "young" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The cow eats the bear.
("cow" "eats" "bear" "+")
int3
The bear is red.
("bear" "is" "red" "+")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2)) triple1) -> (rule5 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule3 % int2)) triple1) -> (rule5 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
The cow eats the bear.
("cow" "eats" "bear" "+")
int4