The bear does not eat the rabbit. The bear is big. The bear is nice. The cat eats the cow. The cat eats the rabbit. The cat is blue. The cat visits the rabbit. The cow eats the cat. The cow likes the rabbit. The cow does not visit the bear. The rabbit likes the cow. All big people are nice. If someone eats the cow then the cow does not visit the cat. If someone eats the bear then the bear visits the cat. If someone eats the cat and they like the cow then they do not like the cat. If someone visits the cat then they like the cat. If someone is big then they do not like the rabbit. If someone visits the cat then the cat is big. If someone is nice then they visit the cat. If someone eats the cow and they are not big then the cow is blue.
The bear does not eat the rabbit.
("bear" "eats" "rabbit" "-")
The bear is big.
("bear" "is" "big" "+")
The bear is nice.
("bear" "is" "nice" "+")
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow does not visit the bear.
("cow" "visits" "bear" "-")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
All big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone eats the cow then the cow does not visit the cat.
((("someone" "eats" "cow" "+")) -> ("cow" "visits" "cat" "-"))
If someone eats the bear then the bear visits the cat.
((("someone" "eats" "bear" "+")) -> ("bear" "visits" "cat" "+"))
If someone eats the cat and they like the cow then they do not like the cat.
((("someone" "eats" "cat" "+") ("someone" "likes" "cow" "+")) -> ("someone" "likes" "cat" "-"))
If someone visits the cat then they like the cat.
((("someone" "visits" "cat" "+")) -> ("someone" "likes" "cat" "+"))
If someone is big then they do not like the rabbit.
((("someone" "is" "big" "+")) -> ("someone" "likes" "rabbit" "-"))
If someone visits the cat then the cat is big.
((("someone" "visits" "cat" "+")) -> ("cat" "is" "big" "+"))
If someone is nice then they visit the cat.
((("someone" "is" "nice" "+")) -> ("someone" "visits" "cat" "+"))
If someone eats the cow and they are not big then the cow is blue.
((("someone" "eats" "cow" "+") ("someone" "is" "big" "~")) -> ("cow" "is" "blue" "+"))
The cow eats the cat.
True
1
proof
[(triple8)]
("cow" "eats" "cat" "+")
triple8
The cat does not eat the cow.
False
1
inv-proof
[(triple4)]
("cat" "eats" "cow" "-")
triple4
The bear visits the cat.
True
2
proof
[(((triple3) -> rule8) OR ((((triple2) -> rule1)) -> rule8))]
("bear" "visits" "cat" "+")
((triple3) -> (rule8 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear likes the rabbit.
False
2
inv-proof
[(((triple2) -> rule6))]
("bear" "likes" "rabbit" "+")
((triple2) -> (rule6 % int1))
The bear does not like the rabbit.
("bear" "likes" "rabbit" "-")
int1
The cat is big.
True
3
proof
[(((((triple3) -> rule8)) -> rule7) OR ((((((triple2) -> rule1)) -> rule8)) -> rule7))]
("cat" "is" "big" "+")
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear does not like the cat.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule5) OR ((((((triple2) -> rule1)) -> rule8)) -> rule5))]
("bear" "likes" "cat" "-")
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The cat is nice.
True
4
proof
[(((((((triple3) -> rule8)) -> rule7)) -> rule1) OR ((((((((triple2) -> rule1)) -> rule8)) -> rule7)) -> rule1))]
("cat" "is" "nice" "+")
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
The cat is not nice.
False
4
inv-proof
[(((((((triple3) -> rule8)) -> rule7)) -> rule1) OR ((((((((triple2) -> rule1)) -> rule8)) -> rule7)) -> rule1))]
("cat" "is" "nice" "-")
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
The cat visits the cat.
True
5
proof
[(((((((((triple3) -> rule8)) -> rule7)) -> rule1)) -> rule8) OR ((((((((((triple2) -> rule1)) -> rule8)) -> rule7)) -> rule1)) -> rule8))]
("cat" "visits" "cat" "+")
((((((((triple3) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
((((((((((triple2) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
The bear is nice.
("bear" "is" "nice" "+")
int5
The cat does not visit the cat.
False
5
inv-proof
[(((((((((triple3) -> rule8)) -> rule7)) -> rule1)) -> rule8) OR ((((((((((triple2) -> rule1)) -> rule8)) -> rule7)) -> rule1)) -> rule8))]
("cat" "visits" "cat" "-")
((((((((triple3) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
((((((((((triple2) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
The bear is nice.
("bear" "is" "nice" "+")
int5
The cat likes the cat.
True
6
proof
[(((((((((((triple3) -> rule8)) -> rule7)) -> rule1)) -> rule8)) -> rule5) OR ((((((((((((triple2) -> rule1)) -> rule8)) -> rule7)) -> rule1)) -> rule8)) -> rule5))]
("cat" "likes" "cat" "+")
((((((((((triple3) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The bear visits the cat.
("bear" "visits" "cat" "+")
int5
((((((((((((triple2) -> (rule1 % int6))) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The bear visits the cat.
("bear" "visits" "cat" "+")
int5
The bear is nice.
("bear" "is" "nice" "+")
int6
The cat does not like the cat.
False
6
inv-proof
[(((((((((((triple3) -> rule8)) -> rule7)) -> rule1)) -> rule8)) -> rule5) OR ((((((((((((triple2) -> rule1)) -> rule8)) -> rule7)) -> rule1)) -> rule8)) -> rule5))]
("cat" "likes" "cat" "-")
((((((((((triple3) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The bear visits the cat.
("bear" "visits" "cat" "+")
int5
((((((((((((triple2) -> (rule1 % int6))) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The bear visits the cat.
("bear" "visits" "cat" "+")
int5
The bear is nice.
("bear" "is" "nice" "+")
int6
The cow is not blue.
Unknown
inv-rconc
[@1: The cow is blue.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("cow" "is" "blue" "-")
The cow likes the cat.
Unknown
rconc
[@1: The cow likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "likes" "cat" "+")
The rabbit does not visit the cat.
Unknown
inv-rconc
[@2: The rabbit visits the cat.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("rabbit" "visits" "cat" "-")
The cow is nice.
Unknown
rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "nice" "+")
The rabbit does not like the cat.
Unknown
inv-rconc
[@3: The rabbit likes the cat.[CWA. Example of deepest failure = (rule5 <- rule8 <- rule1 <- FAIL)]]
("rabbit" "likes" "cat" "-")
The rabbit is nice.
Unknown
rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "nice" "+")
The cow does not eat the rabbit.
Unknown
inv-random
[@0: The cow eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "rabbit" "-")
The bear visits the cow.
Unknown
random
[@0: The bear visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "cow" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The cow eats the bear.
Unknown
random
[@0: The cow eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "bear" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear does not eat the rabbit.[(triple1)] The bear is big.[(triple2)] The bear is nice.[(triple3 OR ((triple2) -> rule1))] The cat eats the cow.[(triple4)] The cat eats the rabbit.[(triple5)] The cat is blue.[(triple6)] The cat visits the rabbit.[(triple7)] The cow does not visit the bear.[(triple10)] The cow eats the cat.[(triple8)] The cow likes the rabbit.[(triple9)] The rabbit likes the cow.[(triple11)] @1: The bear does not like the rabbit.[(((triple2) -> rule6))] The bear visits the cat.[(((triple3) -> rule8) OR ((((triple2) -> rule1)) -> rule8))] The cow does not visit the cat.[(((triple4) -> rule2))] @2: The bear likes the cat.[(((((triple3) -> rule8)) -> rule5) OR ((((((triple2) -> rule1)) -> rule8)) -> rule5))] The cat is big.[(((((triple3) -> rule8)) -> rule7) OR ((((((triple2) -> rule1)) -> rule8)) -> rule7))] @3: The cat does not like the rabbit.[(((((((triple3) -> rule8)) -> rule7)) -> rule6) OR ((((((((triple2) -> rule1)) -> rule8)) -> rule7)) -> rule6))] The cat is nice.[(((((((triple3) -> rule8)) -> rule7)) -> rule1) OR ((((((((triple2) -> rule1)) -> rule8)) -> rule7)) -> rule1))] @4: The cat visits the cat.[(((((((((triple3) -> rule8)) -> rule7)) -> rule1)) -> rule8) OR ((((((((((triple2) -> rule1)) -> rule8)) -> rule7)) -> rule1)) -> rule8))] @5: The cat likes the cat.[(((((((((((triple3) -> rule8)) -> rule7)) -> rule1)) -> rule8)) -> rule5) OR ((((((((((((triple2) -> rule1)) -> rule8)) -> rule7)) -> rule1)) -> rule8)) -> rule5))]
The bear does not eat the rabbit.
("bear" "eats" "rabbit" "-")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is nice.
("bear" "is" "nice" "+")
triple3
((triple2) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
triple4
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple5
The cat is blue.
("cat" "is" "blue" "+")
triple6
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple7
The cow does not visit the bear.
("cow" "visits" "bear" "-")
triple10
The cow eats the cat.
("cow" "eats" "cat" "+")
triple8
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple9
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple11
The bear does not like the rabbit.
("bear" "likes" "rabbit" "-")
((triple2) -> (rule6 % int1))
The bear does not like the rabbit.
("bear" "likes" "rabbit" "-")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
((triple3) -> (rule8 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The cow does not visit the cat.
("cow" "visits" "cat" "-")
((triple4) -> (rule2 % int1))
The cow does not visit the cat.
("cow" "visits" "cat" "-")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The cat is big.
("cat" "is" "big" "+")
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The cat does not like the rabbit.
("cat" "likes" "rabbit" "-")
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The cat does not like the rabbit.
("cat" "likes" "rabbit" "-")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The cat does not like the rabbit.
("cat" "likes" "rabbit" "-")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
The cat is nice.
("cat" "is" "nice" "+")
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
The cat visits the cat.
("cat" "visits" "cat" "+")
((((((((triple3) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
((((((((((triple2) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
The bear is nice.
("bear" "is" "nice" "+")
int5
The cat likes the cat.
("cat" "likes" "cat" "+")
((((((((((triple3) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The bear visits the cat.
("bear" "visits" "cat" "+")
int5
((((((((((((triple2) -> (rule1 % int6))) -> (rule8 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The bear visits the cat.
("bear" "visits" "cat" "+")
int5
The bear is nice.
("bear" "is" "nice" "+")
int6