The dog chases the rabbit. The rabbit is red. The rabbit visits the tiger. The tiger chases the dog. The tiger does not chase the rabbit. The tiger eats the dog. The tiger is not round. If something eats the rabbit and it is red then it is not cold. If the dog eats the rabbit and the dog is round then the dog chases the tiger. If something visits the tiger then it does not eat the tiger. If the rabbit is red and the rabbit does not eat the tiger then the tiger is cold. If something is cold then it does not visit the rabbit. If something visits the rabbit then it chases the rabbit.
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger does not chase the rabbit.
("tiger" "chases" "rabbit" "-")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger is not round.
("tiger" "is" "round" "-")
If something eats the rabbit and it is red then it is not cold.
((("something" "eats" "rabbit" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "-"))
If the dog eats the rabbit and the dog is round then the dog chases the tiger.
((("dog" "eats" "rabbit" "+") ("dog" "is" "round" "+")) -> ("dog" "chases" "tiger" "+"))
If something visits the tiger then it does not eat the tiger.
((("something" "visits" "tiger" "+")) -> ("something" "eats" "tiger" "-"))
If the rabbit is red and the rabbit does not eat the tiger then the tiger is cold.
((("rabbit" "is" "red" "+") ("rabbit" "eats" "tiger" "~")) -> ("tiger" "is" "cold" "+"))
If something is cold then it does not visit the rabbit.
((("something" "is" "cold" "+")) -> ("something" "visits" "rabbit" "-"))
If something visits the rabbit then it chases the rabbit.
((("something" "visits" "rabbit" "+")) -> ("something" "chases" "rabbit" "+"))
The rabbit is red.
True
1
proof
[(triple2)]
("rabbit" "is" "red" "+")
triple2
The tiger is round.
False
1
inv-proof
[(triple7)]
("tiger" "is" "round" "+")
triple7
The rabbit does not eat the tiger.
True
2
proof
[(((triple3) -> rule3))]
("rabbit" "eats" "tiger" "-")
((triple3) -> (rule3 % int1))
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
int1
The rabbit eats the tiger.
False
2
inv-proof
[(((triple3) -> rule3))]
("rabbit" "eats" "tiger" "+")
((triple3) -> (rule3 % int1))
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
int1
The tiger is cold.
True
4
proof
[(((triple2 ((triple3) -> rule3)) -> rule4))]
("tiger" "is" "cold" "+")
((triple2 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
int2
The tiger is not cold.
False
4
inv-proof
[(((triple2 ((triple3) -> rule3)) -> rule4))]
("tiger" "is" "cold" "-")
((triple2 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
int2
The tiger does not visit the rabbit.
True
5
proof
[(((((triple2 ((triple3) -> rule3)) -> rule4)) -> rule5))]
("tiger" "visits" "rabbit" "-")
((((triple2 ((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger does not visit the rabbit.
("tiger" "visits" "rabbit" "-")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
int3
The tiger visits the rabbit.
False
5
inv-proof
[(((((triple2 ((triple3) -> rule3)) -> rule4)) -> rule5))]
("tiger" "visits" "rabbit" "+")
((((triple2 ((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger does not visit the rabbit.
("tiger" "visits" "rabbit" "-")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
int3
The dog does not chase the tiger.
Unknown
inv-rconc
[@1: The dog chases the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "tiger" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
The dog does not eat the rabbit.
Unknown
inv-random
[@0: The dog eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "rabbit" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The rabbit eats the dog.
Unknown
random
[@0: The rabbit eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "dog" "+")
@0: The dog chases the rabbit.[(triple1)] The rabbit is red.[(triple2)] The rabbit visits the tiger.[(triple3)] The tiger chases the dog.[(triple4)] The tiger does not chase the rabbit.[(triple5)] The tiger eats the dog.[(triple6)] The tiger is not round.[(triple7)] @1: The rabbit does not eat the tiger.[(((triple3) -> rule3))] @2: The tiger is cold.[(((triple2 ((triple3) -> rule3)) -> rule4))] @3: The tiger does not visit the rabbit.[(((((triple2 ((triple3) -> rule3)) -> rule4)) -> rule5))]
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple1
The rabbit is red.
("rabbit" "is" "red" "+")
triple2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple3
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple4
The tiger does not chase the rabbit.
("tiger" "chases" "rabbit" "-")
triple5
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple6
The tiger is not round.
("tiger" "is" "round" "-")
triple7
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
((triple3) -> (rule3 % int1))
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((triple2 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
int2
The tiger does not visit the rabbit.
("tiger" "visits" "rabbit" "-")
((((triple2 ((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger does not visit the rabbit.
("tiger" "visits" "rabbit" "-")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
int3