The dog is cold. The dog is kind. The dog is red. The dog is rough. The dog is round. The dog likes the rabbit. The dog needs the rabbit. The dog sees the rabbit. The rabbit is cold. The rabbit is kind. The rabbit is red. The rabbit is rough. The rabbit is round. The rabbit likes the dog. The rabbit needs the dog. The rabbit sees the dog. If someone is red and rough then they like the dog. If someone is red and not kind then they need the dog. If someone is kind and they like the dog then they need the dog. If someone is kind and not red then they need the rabbit. If the dog likes the rabbit then the rabbit likes the dog. If someone sees the rabbit and they are not rough then they are cold. If someone is cold then they like the rabbit. If someone needs the dog then they see the dog.
The dog is cold.
("dog" "is" "cold" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is round.
("dog" "is" "round" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If someone is red and rough then they like the dog.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "likes" "dog" "+"))
If someone is red and not kind then they need the dog.
((("someone" "is" "red" "+") ("someone" "is" "kind" "~")) -> ("someone" "needs" "dog" "+"))
If someone is kind and they like the dog then they need the dog.
((("someone" "is" "kind" "+") ("someone" "likes" "dog" "+")) -> ("someone" "needs" "dog" "+"))
If someone is kind and not red then they need the rabbit.
((("someone" "is" "kind" "+") ("someone" "is" "red" "~")) -> ("someone" "needs" "rabbit" "+"))
If the dog likes the rabbit then the rabbit likes the dog.
((("dog" "likes" "rabbit" "+")) -> ("rabbit" "likes" "dog" "+"))
If someone sees the rabbit and they are not rough then they are cold.
((("someone" "sees" "rabbit" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "cold" "+"))
If someone is cold then they like the rabbit.
((("someone" "is" "cold" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone needs the dog then they see the dog.
((("someone" "needs" "dog" "+")) -> ("someone" "sees" "dog" "+"))
The rabbit is rough.
True
1
proof
[(triple12)]
("rabbit" "is" "rough" "+")
triple12
The dog is not round.
False
1
inv-proof
[(triple5)]
("dog" "is" "round" "-")
triple5
The rabbit likes the rabbit.
True
2
proof
[(((triple9) -> rule7))]
("rabbit" "likes" "rabbit" "+")
((triple9) -> (rule7 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit does not like the rabbit.
False
2
inv-proof
[(((triple9) -> rule7))]
("rabbit" "likes" "rabbit" "-")
((triple9) -> (rule7 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The dog needs the dog.
True
5
proof
[(((triple2 ((triple3 triple4) -> rule1)) -> rule3))]
("dog" "needs" "dog" "+")
((triple2 ((triple3 triple4) -> (rule1 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog does not need the dog.
False
5
inv-proof
[(((triple2 ((triple3 triple4) -> rule1)) -> rule3))]
("dog" "needs" "dog" "-")
((triple2 ((triple3 triple4) -> (rule1 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog sees the dog.
True
6
proof
[(((((triple2 ((triple3 triple4) -> rule1)) -> rule3)) -> rule8))]
("dog" "sees" "dog" "+")
((((triple2 ((triple3 triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3
The dog does not see the dog.
False
6
inv-proof
[(((((triple2 ((triple3 triple4) -> rule1)) -> rule3)) -> rule8))]
("dog" "sees" "dog" "-")
((((triple2 ((triple3 triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The dog is cold.[(triple1)] The dog is kind.[(triple2)] The dog is red.[(triple3)] The dog is rough.[(triple4)] The dog is round.[(triple5)] The dog likes the rabbit.[(triple6 OR ((triple1) -> rule7))] The dog needs the rabbit.[(triple7)] The dog sees the rabbit.[(triple8)] The rabbit is cold.[(triple9)] The rabbit is kind.[(triple10)] The rabbit is red.[(triple11)] The rabbit is rough.[(triple12)] The rabbit is round.[(triple13)] The rabbit likes the dog.[(triple14 OR ((triple6) -> rule5) OR ((triple11 triple12) -> rule1) OR ((((triple1) -> rule7)) -> rule5))] The rabbit needs the dog.[(triple15 OR ((triple10 triple14) -> rule3) OR ((triple10 ((triple6) -> rule5)) -> rule3) OR ((triple10 ((triple11 triple12) -> rule1)) -> rule3) OR ((triple10 ((((triple1) -> rule7)) -> rule5)) -> rule3))] The rabbit sees the dog.[(triple16 OR ((triple15) -> rule8) OR ((((triple10 triple14) -> rule3)) -> rule8) OR ((((triple10 ((triple6) -> rule5)) -> rule3)) -> rule8) OR ((((triple10 ((triple11 triple12) -> rule1)) -> rule3)) -> rule8) OR ((((triple10 ((((triple1) -> rule7)) -> rule5)) -> rule3)) -> rule8))] @1: The dog likes the dog.[(((triple3 triple4) -> rule1))] The rabbit likes the rabbit.[(((triple9) -> rule7))] @2: The dog needs the dog.[(((triple2 ((triple3 triple4) -> rule1)) -> rule3))] @3: The dog sees the dog.[(((((triple2 ((triple3 triple4) -> rule1)) -> rule3)) -> rule8))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
triple2
The dog is red.
("dog" "is" "red" "+")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple5
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple6
((triple1) -> (rule7 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple7
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple8
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple9
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple10
The rabbit is red.
("rabbit" "is" "red" "+")
triple11
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple12
The rabbit is round.
("rabbit" "is" "round" "+")
triple13
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple14
((triple6) -> (rule5 % int1))
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int1
((triple11 triple12) -> (rule1 % int1))
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple15
((triple10 triple14) -> (rule3 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
((triple10 ((triple6) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int2
((triple10 ((triple11 triple12) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int2
((triple10 ((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int3
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple16
((triple15) -> (rule8 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
((((triple10 triple14) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
((((triple10 ((triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int3
((((triple10 ((triple11 triple12) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int3
((((triple10 ((((triple1) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int3
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int4
The dog likes the dog.
("dog" "likes" "dog" "+")
((triple3 triple4) -> (rule1 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple9) -> (rule7 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple2 ((triple3 triple4) -> (rule1 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
((((triple2 ((triple3 triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3