The cow is big. The cow is green. The cow is rough. The cow is round. The cow is young. The cow needs the rabbit. The cow sees the rabbit. The cow visits the rabbit. The rabbit is big. The rabbit is green. The rabbit is rough. The rabbit is round. The rabbit is young. The rabbit needs the cow. The rabbit sees the cow. The rabbit visits the cow. If the cow sees the rabbit then the rabbit needs the cow. If someone visits the cow and the cow visits the rabbit then the rabbit needs the cow. If someone needs the cow then they see the cow. If someone is big then they visit the cow. If someone needs the cow and they are round then the cow visits the rabbit. All green people are big. If someone is young then they visit the rabbit. If the rabbit is young and the rabbit needs the cow then the rabbit visits the cow.
The cow is big.
("cow" "is" "big" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is round.
("cow" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If the cow sees the rabbit then the rabbit needs the cow.
((("cow" "sees" "rabbit" "+")) -> ("rabbit" "needs" "cow" "+"))
If someone visits the cow and the cow visits the rabbit then the rabbit needs the cow.
((("someone" "visits" "cow" "+") ("cow" "visits" "rabbit" "+")) -> ("rabbit" "needs" "cow" "+"))
If someone needs the cow then they see the cow.
((("someone" "needs" "cow" "+")) -> ("someone" "sees" "cow" "+"))
If someone is big then they visit the cow.
((("someone" "is" "big" "+")) -> ("someone" "visits" "cow" "+"))
If someone needs the cow and they are round then the cow visits the rabbit.
((("someone" "needs" "cow" "+") ("someone" "is" "round" "+")) -> ("cow" "visits" "rabbit" "+"))
All green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is young then they visit the rabbit.
((("someone" "is" "young" "+")) -> ("someone" "visits" "rabbit" "+"))
If the rabbit is young and the rabbit needs the cow then the rabbit visits the cow.
((("rabbit" "is" "young" "+") ("rabbit" "needs" "cow" "+")) -> ("rabbit" "visits" "cow" "+"))
The rabbit is round.
True
1
proof
[(triple12)]
("rabbit" "is" "round" "+")
triple12
The cow is not big.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule6))]
("cow" "is" "big" "-")
triple1
((triple2) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow does not see the cow.
Unknown
inv-rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "sees" "cow" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow is big.[(triple1 OR ((triple2) -> rule6))] The cow is green.[(triple2)] The cow is rough.[(triple3)] The cow is round.[(triple4)] The cow is young.[(triple5)] The cow needs the rabbit.[(triple6)] The cow sees the rabbit.[(triple7)] The cow visits the rabbit.[(triple8 OR ((triple5) -> rule7) OR ((triple14 triple12) -> rule5) OR ((((triple7) -> rule1) triple12) -> rule5))] The rabbit is big.[(triple9 OR ((triple10) -> rule6))] The rabbit is green.[(triple10)] The rabbit is rough.[(triple11)] The rabbit is round.[(triple12)] The rabbit is young.[(triple13)] The rabbit needs the cow.[(triple14 OR ((triple7) -> rule1) OR ((triple16 triple8) -> rule2) OR ((triple16 ((triple5) -> rule7)) -> rule2) OR ((((triple1) -> rule4) triple8) -> rule2) OR ((((triple9) -> rule4) triple8) -> rule2) OR ((((triple1) -> rule4) ((triple5) -> rule7)) -> rule2) OR ((((triple9) -> rule4) ((triple5) -> rule7)) -> rule2) OR ((((((triple10) -> rule6)) -> rule4) triple8) -> rule2) OR ((((((triple2) -> rule6)) -> rule4) triple8) -> rule2) OR ((((((triple10) -> rule6)) -> rule4) ((triple5) -> rule7)) -> rule2) OR ((((((triple2) -> rule6)) -> rule4) ((triple5) -> rule7)) -> rule2))] The rabbit sees the cow.[(triple15 OR ((triple14) -> rule3) OR ((((triple7) -> rule1)) -> rule3) OR ((((triple16 triple8) -> rule2)) -> rule3) OR ((((triple16 ((triple5) -> rule7)) -> rule2)) -> rule3) OR ((((((triple1) -> rule4) triple8) -> rule2)) -> rule3) OR ((((((triple9) -> rule4) triple8) -> rule2)) -> rule3) OR ((((((triple1) -> rule4) ((triple5) -> rule7)) -> rule2)) -> rule3) OR ((((((triple9) -> rule4) ((triple5) -> rule7)) -> rule2)) -> rule3) OR ((((((((triple10) -> rule6)) -> rule4) triple8) -> rule2)) -> rule3) OR ((((((((triple2) -> rule6)) -> rule4) triple8) -> rule2)) -> rule3) OR ((((((((triple10) -> rule6)) -> rule4) ((triple5) -> rule7)) -> rule2)) -> rule3) OR ((((((((triple2) -> rule6)) -> rule4) ((triple5) -> rule7)) -> rule2)) -> rule3))] The rabbit visits the cow.[(triple16 OR ((triple9) -> rule4) OR ((triple13 triple14) -> rule8) OR ((((triple10) -> rule6)) -> rule4) OR ((triple13 ((triple7) -> rule1)) -> rule8) OR ((triple13 ((((triple1) -> rule4) triple8) -> rule2)) -> rule8) OR ((triple13 ((((triple1) -> rule4) ((triple5) -> rule7)) -> rule2)) -> rule8) OR ((triple13 ((((((triple2) -> rule6)) -> rule4) triple8) -> rule2)) -> rule8) OR ((triple13 ((((((triple2) -> rule6)) -> rule4) ((triple5) -> rule7)) -> rule2)) -> rule8))] @1: The cow visits the cow.[(((triple1) -> rule4) OR ((((triple2) -> rule6)) -> rule4))] The rabbit visits the rabbit.[(((triple13) -> rule7))]
The cow is big.
("cow" "is" "big" "+")
triple1
((triple2) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is green.
("cow" "is" "green" "+")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple3
The cow is round.
("cow" "is" "round" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple6
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple7
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple8
((triple5) -> (rule7 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
((triple14 triple12) -> (rule5 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
((((triple7) -> (rule1 % int2)) triple12) -> (rule5 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
triple9
((triple10) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
triple10
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple11
The rabbit is round.
("rabbit" "is" "round" "+")
triple12
The rabbit is young.
("rabbit" "is" "young" "+")
triple13
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple14
((triple7) -> (rule1 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
((triple16 triple8) -> (rule2 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
((triple16 ((triple5) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int2
((((triple1) -> (rule4 % int2)) triple8) -> (rule2 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
((((triple9) -> (rule4 % int2)) triple8) -> (rule2 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
((((triple1) -> (rule4 % int3)) ((triple5) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
((((triple9) -> (rule4 % int3)) ((triple5) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3
((((((triple10) -> (rule6 % int3))) -> (rule4 % int2)) triple8) -> (rule2 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2)) triple8) -> (rule2 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
((((((triple10) -> (rule6 % int4))) -> (rule4 % int3)) ((triple5) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3
The rabbit is big.
("rabbit" "is" "big" "+")
int4
((((((triple2) -> (rule6 % int4))) -> (rule4 % int3)) ((triple5) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple15
((triple14) -> (rule3 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
((((triple16 triple8) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
((((triple16 ((triple5) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int3
((((((triple1) -> (rule4 % int3)) triple8) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
((((((triple9) -> (rule4 % int3)) triple8) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3
((((((triple1) -> (rule4 % int4)) ((triple5) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int3
The cow visits the cow.
("cow" "visits" "cow" "+")
int4
((((((triple9) -> (rule4 % int4)) ((triple5) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int3
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int4
((((((((triple10) -> (rule6 % int4))) -> (rule4 % int3)) triple8) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3
The rabbit is big.
("rabbit" "is" "big" "+")
int4
((((((((triple2) -> (rule6 % int4))) -> (rule4 % int3)) triple8) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
((((((((triple10) -> (rule6 % int5))) -> (rule4 % int4)) ((triple5) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int3
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int4
The rabbit is big.
("rabbit" "is" "big" "+")
int5
((((((((triple2) -> (rule6 % int5))) -> (rule4 % int4)) ((triple5) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int3
The cow visits the cow.
("cow" "visits" "cow" "+")
int4
The cow is big.
("cow" "is" "big" "+")
int5
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple16
((triple9) -> (rule4 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
((triple13 triple14) -> (rule8 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
((triple13 ((triple7) -> (rule1 % int2))) -> (rule8 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
((triple13 ((((triple1) -> (rule4 % int3)) triple8) -> (rule2 % int2))) -> (rule8 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
((triple13 ((((triple1) -> (rule4 % int4)) ((triple5) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int3
The cow visits the cow.
("cow" "visits" "cow" "+")
int4
((triple13 ((((((triple2) -> (rule6 % int4))) -> (rule4 % int3)) triple8) -> (rule2 % int2))) -> (rule8 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
((triple13 ((((((triple2) -> (rule6 % int5))) -> (rule4 % int4)) ((triple5) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int3
The cow visits the cow.
("cow" "visits" "cow" "+")
int4
The cow is big.
("cow" "is" "big" "+")
int5
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple1) -> (rule4 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple13) -> (rule7 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1