The cow eats the rabbit. The cow is blue. The cow is cold. The cow is green. The cow is nice. The cow is round. The cow sees the rabbit. The cow visits the rabbit. The rabbit eats the cow. The rabbit is blue. The rabbit is cold. The rabbit is green. The rabbit is nice. The rabbit is round. The rabbit sees the cow. The rabbit visits the cow. If the rabbit is round and the rabbit visits the cow then the cow visits the rabbit. If something eats the cow then the cow is nice. If something is round then it sees the cow. If the cow visits the rabbit and the rabbit is round then the rabbit sees the cow. If something sees the cow then the cow sees the rabbit. If something visits the cow and the cow eats the rabbit then it is nice.
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is round.
("cow" "is" "round" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If the rabbit is round and the rabbit visits the cow then the cow visits the rabbit.
((("rabbit" "is" "round" "+") ("rabbit" "visits" "cow" "+")) -> ("cow" "visits" "rabbit" "+"))
If something eats the cow then the cow is nice.
((("something" "eats" "cow" "+")) -> ("cow" "is" "nice" "+"))
If something is round then it sees the cow.
((("something" "is" "round" "+")) -> ("something" "sees" "cow" "+"))
If the cow visits the rabbit and the rabbit is round then the rabbit sees the cow.
((("cow" "visits" "rabbit" "+") ("rabbit" "is" "round" "+")) -> ("rabbit" "sees" "cow" "+"))
If something sees the cow then the cow sees the rabbit.
((("something" "sees" "cow" "+")) -> ("cow" "sees" "rabbit" "+"))
If something visits the cow and the cow eats the rabbit then it is nice.
((("something" "visits" "cow" "+") ("cow" "eats" "rabbit" "+")) -> ("something" "is" "nice" "+"))
The cow visits the rabbit.
True
1
proof
[(triple8 OR ((triple14 triple16) -> rule1))]
("cow" "visits" "rabbit" "+")
triple8
((triple14 triple16) -> (rule1 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
The cow is not round.
False
1
inv-proof
[(triple6)]
("cow" "is" "round" "-")
triple6
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow eats the rabbit.[(triple1)] The cow is blue.[(triple2)] The cow is cold.[(triple3)] The cow is green.[(triple4)] The cow is nice.[(triple5 OR ((triple9) -> rule2))] The cow is round.[(triple6)] The cow sees the rabbit.[(triple7 OR ((triple15) -> rule5) OR ((((triple14) -> rule3)) -> rule5) OR ((((triple6) -> rule3)) -> rule5) OR ((((triple8 triple14) -> rule4)) -> rule5) OR ((((((triple14 triple16) -> rule1) triple14) -> rule4)) -> rule5))] The cow visits the rabbit.[(triple8 OR ((triple14 triple16) -> rule1))] The rabbit eats the cow.[(triple9)] The rabbit is blue.[(triple10)] The rabbit is cold.[(triple11)] The rabbit is green.[(triple12)] The rabbit is nice.[(triple13 OR ((triple16 triple1) -> rule6))] The rabbit is round.[(triple14)] The rabbit sees the cow.[(triple15 OR ((triple14) -> rule3) OR ((triple8 triple14) -> rule4) OR ((((triple14 triple16) -> rule1) triple14) -> rule4))] The rabbit visits the cow.[(triple16)] @1: The cow sees the cow.[(((triple6) -> rule3))]
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple3
The cow is green.
("cow" "is" "green" "+")
triple4
The cow is nice.
("cow" "is" "nice" "+")
triple5
((triple9) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is round.
("cow" "is" "round" "+")
triple6
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple7
((triple15) -> (rule5 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
((((triple14) -> (rule3 % int2))) -> (rule5 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule5 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
((((triple8 triple14) -> (rule4 % int2))) -> (rule5 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int2
((((((triple14 triple16) -> (rule1 % int3)) triple14) -> (rule4 % int2))) -> (rule5 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int2
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int3
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple8
((triple14 triple16) -> (rule1 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple9
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple10
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple11
The rabbit is green.
("rabbit" "is" "green" "+")
triple12
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple13
((triple16 triple1) -> (rule6 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
triple14
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple15
((triple14) -> (rule3 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
((triple8 triple14) -> (rule4 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
((((triple14 triple16) -> (rule1 % int2)) triple14) -> (rule4 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple16
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple6) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1