The dog eats the rabbit. The dog is big. The dog is kind. The dog is rough. The dog is round. The dog needs the rabbit. The dog sees the rabbit. The rabbit eats the dog. The rabbit is big. The rabbit needs the dog. If something is round then it needs the dog. If something needs the dog then the dog eats the rabbit. If something is round then it needs the rabbit. If something eats the rabbit then it sees the rabbit. If something eats the dog and the dog needs the rabbit then the rabbit needs the dog. If the dog eats the rabbit and the rabbit sees 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 kind.
("dog" "is" "kind" "+")
The dog is 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 big.
("rabbit" "is" "big" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
If something is round then it needs the dog.
((("something" "is" "round" "+")) -> ("something" "needs" "dog" "+"))
If something needs the dog then the dog eats the rabbit.
((("something" "needs" "dog" "+")) -> ("dog" "eats" "rabbit" "+"))
If something is round then it needs the rabbit.
((("something" "is" "round" "+")) -> ("something" "needs" "rabbit" "+"))
If something eats the rabbit then it sees the rabbit.
((("something" "eats" "rabbit" "+")) -> ("something" "sees" "rabbit" "+"))
If something eats the dog and the dog needs the rabbit then the rabbit needs the dog.
((("something" "eats" "dog" "+") ("dog" "needs" "rabbit" "+")) -> ("rabbit" "needs" "dog" "+"))
If the dog eats the rabbit and the rabbit sees the dog then the dog sees the rabbit.
((("dog" "eats" "rabbit" "+") ("rabbit" "sees" "dog" "+")) -> ("dog" "sees" "rabbit" "+"))
The dog sees the rabbit.
True
1
proof
[(triple7 OR ((triple1) -> rule4) OR ((((triple10) -> rule2)) -> rule4) OR ((((((triple5) -> rule1)) -> rule2)) -> rule4) OR ((((((triple8 triple6) -> rule5)) -> rule2)) -> rule4) OR ((((((triple8 ((triple5) -> rule3)) -> rule5)) -> rule2)) -> rule4))]
("dog" "sees" "rabbit" "+")
triple7
((triple1) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
int3
((((((triple8 triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int3
((((((triple8 ((triple5) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int3
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int4
The rabbit is not big.
False
1
inv-proof
[(triple9)]
("rabbit" "is" "big" "-")
triple9
The dog needs the dog.
True
2
proof
[(((triple5) -> rule1))]
("dog" "needs" "dog" "+")
((triple5) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog does not need the dog.
False
2
inv-proof
[(((triple5) -> rule1))]
("dog" "needs" "dog" "-")
((triple5) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit sees the rabbit.
Unknown
rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "sees" "rabbit" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
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 ((triple10) -> rule2) OR ((((triple5) -> rule1)) -> rule2) OR ((((triple8 triple6) -> rule5)) -> rule2) OR ((((triple8 ((triple5) -> rule3)) -> rule5)) -> rule2))] The dog is big.[(triple2)] The dog is kind.[(triple3)] The dog is rough.[(triple4)] The dog is round.[(triple5)] The dog needs the rabbit.[(triple6 OR ((triple5) -> rule3))] The dog sees the rabbit.[(triple7 OR ((triple1) -> rule4) OR ((((triple10) -> rule2)) -> rule4) OR ((((((triple5) -> rule1)) -> rule2)) -> rule4) OR ((((((triple8 triple6) -> rule5)) -> rule2)) -> rule4) OR ((((((triple8 ((triple5) -> rule3)) -> rule5)) -> rule2)) -> rule4))] The rabbit eats the dog.[(triple8)] The rabbit is big.[(triple9)] The rabbit needs the dog.[(triple10 OR ((triple8 triple6) -> rule5) OR ((triple8 ((triple5) -> rule3)) -> rule5))] @1: The dog needs the dog.[(((triple5) -> rule1))]
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple1
((triple10) -> (rule2 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
((((triple8 triple6) -> (rule5 % int2))) -> (rule2 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
((((triple8 ((triple5) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int3
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple5
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple6
((triple5) -> (rule3 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple7
((triple1) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
int3
((((((triple8 triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int3
((((((triple8 ((triple5) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int3
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int4
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple8
The rabbit is big.
("rabbit" "is" "big" "+")
triple9
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple10
((triple8 triple6) -> (rule5 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
((triple8 ((triple5) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple5) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1