The dog eats the rabbit. The dog is blue. The dog is cold. The dog is green. The dog is not rough. The dog is round. The dog needs the rabbit. The dog sees the rabbit. The rabbit eats the dog. The rabbit is blue. The rabbit is not cold. The rabbit is green. The rabbit is round. The rabbit needs the dog. The rabbit sees the dog. If something is blue and not round then it needs the dog. If the rabbit needs the dog then the dog needs the rabbit. If the dog is blue then the dog needs the rabbit. If something needs the rabbit and it eats the rabbit then the rabbit needs the dog. All cold things are green. If something is blue then it needs the rabbit. If something needs the dog and the dog eats the rabbit then it sees the rabbit. If something is round and it does not need the dog then it eats the dog.
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is not rough.
("dog" "is" "rough" "-")
The dog is round.
("dog" "is" "round" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is not cold.
("rabbit" "is" "cold" "-")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If something is blue and not round then it needs the dog.
((("something" "is" "blue" "+") ("something" "is" "round" "~")) -> ("something" "needs" "dog" "+"))
If the rabbit needs the dog then the dog needs the rabbit.
((("rabbit" "needs" "dog" "+")) -> ("dog" "needs" "rabbit" "+"))
If the dog is blue then the dog needs the rabbit.
((("dog" "is" "blue" "+")) -> ("dog" "needs" "rabbit" "+"))
If something needs the rabbit and it eats the rabbit then the rabbit needs the dog.
((("something" "needs" "rabbit" "+") ("something" "eats" "rabbit" "+")) -> ("rabbit" "needs" "dog" "+"))
All cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is blue then it needs the rabbit.
((("something" "is" "blue" "+")) -> ("something" "needs" "rabbit" "+"))
If something needs the dog and the dog eats the rabbit then it sees the rabbit.
((("something" "needs" "dog" "+") ("dog" "eats" "rabbit" "+")) -> ("something" "sees" "rabbit" "+"))
If something is round and it does not need the dog then it eats the dog.
((("something" "is" "round" "+") ("something" "needs" "dog" "~")) -> ("something" "eats" "dog" "+"))
The dog is not rough.
True
1
proof
[(triple5)]
("dog" "is" "rough" "-")
triple5
The dog is rough.
False
1
inv-proof
[(triple5)]
("dog" "is" "rough" "+")
triple5
The rabbit sees the rabbit.
True
3
proof
[(((triple14 triple1) -> rule7) OR ((((triple7 triple1) -> rule4) triple1) -> rule7) OR ((((((triple2) -> rule3) triple1) -> rule4) triple1) -> rule7) OR ((((((triple2) -> rule6) triple1) -> rule4) triple1) -> rule7))]
("rabbit" "sees" "rabbit" "+")
((triple14 triple1) -> (rule7 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
((((triple7 triple1) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
((((((triple2) -> (rule3 % int3)) triple1) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int3
((((((triple2) -> (rule6 % int3)) triple1) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int3
The rabbit does not need the rabbit.
False
2
inv-proof
[(((triple10) -> rule6))]
("rabbit" "needs" "rabbit" "-")
((triple10) -> (rule6 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "needs" "dog" "-")
The dog eats the dog.
Unknown
rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "eats" "dog" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The dog eats the rabbit.[(triple1)] The dog is blue.[(triple2)] The dog is cold.[(triple3)] The dog is green.[(triple4 OR ((triple3) -> rule5))] The dog is not rough.[(triple5)] The dog is round.[(triple6)] The dog needs the rabbit.[(triple7 OR ((triple14) -> rule2) OR ((triple2) -> rule3) OR ((triple2) -> rule6))] The dog sees the rabbit.[(triple8)] The rabbit eats the dog.[(triple9)] The rabbit is blue.[(triple10)] The rabbit is green.[(triple12)] The rabbit is not cold.[(triple11)] The rabbit is round.[(triple13)] The rabbit needs the dog.[(triple14 OR ((triple7 triple1) -> rule4) OR ((((triple2) -> rule3) triple1) -> rule4) OR ((((triple2) -> rule6) triple1) -> rule4))] The rabbit sees the dog.[(triple15)] @1: The rabbit needs the rabbit.[(((triple10) -> rule6))] The rabbit sees the rabbit.[(((triple14 triple1) -> rule7) OR ((((triple7 triple1) -> rule4) triple1) -> rule7) OR ((((((triple2) -> rule3) triple1) -> rule4) triple1) -> rule7) OR ((((((triple2) -> rule6) triple1) -> rule4) triple1) -> rule7))]
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is green.
("dog" "is" "green" "+")
triple4
((triple3) -> (rule5 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is not rough.
("dog" "is" "rough" "-")
triple5
The dog is round.
("dog" "is" "round" "+")
triple6
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple7
((triple14) -> (rule2 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
((triple2) -> (rule3 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
((triple2) -> (rule6 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple8
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple9
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple10
The rabbit is green.
("rabbit" "is" "green" "+")
triple12
The rabbit is not cold.
("rabbit" "is" "cold" "-")
triple11
The rabbit is round.
("rabbit" "is" "round" "+")
triple13
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple14
((triple7 triple1) -> (rule4 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
((((triple2) -> (rule3 % int2)) triple1) -> (rule4 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int2
((((triple2) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple15
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple10) -> (rule6 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple14 triple1) -> (rule7 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
((((triple7 triple1) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
((((((triple2) -> (rule3 % int3)) triple1) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int3
((((((triple2) -> (rule6 % int3)) triple1) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int3