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