The dog is not blue. The dog is round. The dog likes the tiger. The dog sees the tiger. The dog visits the tiger. The tiger is blue. The tiger does not visit the dog. If the tiger visits the dog then the tiger sees the dog. If the tiger is kind then the tiger likes the dog. All blue people are round. If someone sees the dog then they are not kind. If someone likes the tiger then they visit the tiger. If someone is round then they see the tiger. If someone visits the tiger then they visit the dog. If someone sees the tiger and the tiger does not visit the dog then they are not green.
The dog is not blue.
("dog" "is" "blue" "-")
The dog is round.
("dog" "is" "round" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger does not visit the dog.
("tiger" "visits" "dog" "-")
If the tiger visits the dog then the tiger sees the dog.
((("tiger" "visits" "dog" "+")) -> ("tiger" "sees" "dog" "+"))
If the tiger is kind then the tiger likes the dog.
((("tiger" "is" "kind" "+")) -> ("tiger" "likes" "dog" "+"))
All blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone sees the dog then they are not kind.
((("someone" "sees" "dog" "+")) -> ("someone" "is" "kind" "-"))
If someone likes the tiger then they visit the tiger.
((("someone" "likes" "tiger" "+")) -> ("someone" "visits" "tiger" "+"))
If someone is round then they see the tiger.
((("someone" "is" "round" "+")) -> ("someone" "sees" "tiger" "+"))
If someone visits the tiger then they visit the dog.
((("someone" "visits" "tiger" "+")) -> ("someone" "visits" "dog" "+"))
If someone sees the tiger and the tiger does not visit the dog then they are not green.
((("someone" "sees" "tiger" "+") ("tiger" "visits" "dog" "~")) -> ("someone" "is" "green" "-"))
The dog visits the tiger.
True
1
proof
[(triple5 OR ((triple3) -> rule5))]
("dog" "visits" "tiger" "+")
triple5
((triple3) -> (rule5 % int1))
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int1
The dog does not see the tiger.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule6))]
("dog" "sees" "tiger" "-")
triple4
((triple2) -> (rule6 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The dog visits the dog.
True
2
proof
[(((triple5) -> rule7) OR ((((triple3) -> rule5)) -> rule7))]
("dog" "visits" "dog" "+")
((triple5) -> (rule7 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int2
The dog does not visit the dog.
False
2
inv-proof
[(((triple5) -> rule7) OR ((((triple3) -> rule5)) -> rule7))]
("dog" "visits" "dog" "-")
((triple5) -> (rule7 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int2
The tiger sees the tiger.
True
3
proof
[(((((triple6) -> rule3)) -> rule6))]
("tiger" "sees" "tiger" "+")
((((triple6) -> (rule3 % int2))) -> (rule6 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger does not see the tiger.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule6))]
("tiger" "sees" "tiger" "-")
((((triple6) -> (rule3 % int2))) -> (rule6 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is not green.
True
5
proof
[(((((((triple6) -> rule3)) -> rule6) triple7) -> rule8))]
("tiger" "is" "green" "-")
((((((triple6) -> (rule3 % int3))) -> (rule6 % int2)) triple7) -> (rule8 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger is green.
False
5
inv-proof
[(((((((triple6) -> rule3)) -> rule6) triple7) -> rule8))]
("tiger" "is" "green" "+")
((((((triple6) -> (rule3 % int3))) -> (rule6 % int2)) triple7) -> (rule8 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger does not like the dog.
Unknown
inv-rconc
[@1: The tiger likes the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "likes" "dog" "-")
The tiger visits the tiger.
Unknown
rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "visits" "tiger" "+")
The tiger does not see the dog.
Unknown
inv-rconc
[@1: The tiger sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "dog" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
@0: The dog is not blue.[(triple1)] The dog is round.[(triple2)] The dog likes the tiger.[(triple3)] The dog sees the tiger.[(triple4 OR ((triple2) -> rule6))] The dog visits the tiger.[(triple5 OR ((triple3) -> rule5))] The tiger does not visit the dog.[(triple7)] The tiger is blue.[(triple6)] @1: The dog is not green.[(((triple4 triple7) -> rule8) OR ((((triple2) -> rule6) triple7) -> rule8))] The dog visits the dog.[(((triple5) -> rule7) OR ((((triple3) -> rule5)) -> rule7))] The tiger is round.[(((triple6) -> rule3))] @2: The tiger sees the tiger.[(((((triple6) -> rule3)) -> rule6))] @3: The tiger is not green.[(((((((triple6) -> rule3)) -> rule6) triple7) -> rule8))]
The dog is not blue.
("dog" "is" "blue" "-")
triple1
The dog is round.
("dog" "is" "round" "+")
triple2
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple3
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple4
((triple2) -> (rule6 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple5
((triple3) -> (rule5 % int1))
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int1
The tiger does not visit the dog.
("tiger" "visits" "dog" "-")
triple7
The tiger is blue.
("tiger" "is" "blue" "+")
triple6
The dog is not green.
("dog" "is" "green" "-")
((triple4 triple7) -> (rule8 % int1))
The dog is not green.
("dog" "is" "green" "-")
int1
((((triple2) -> (rule6 % int2)) triple7) -> (rule8 % int1))
The dog is not green.
("dog" "is" "green" "-")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple5) -> (rule7 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
((triple6) -> (rule3 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((triple6) -> (rule3 % int2))) -> (rule6 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is not green.
("tiger" "is" "green" "-")
((((((triple6) -> (rule3 % int3))) -> (rule6 % int2)) triple7) -> (rule8 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3