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