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