The dog is blue. The dog is green. The dog is kind. The dog is round. The dog is young. The dog likes the tiger. The dog sees the tiger. The dog visits the tiger. The tiger is blue. The tiger is green. The tiger is kind. The tiger is round. The tiger likes the dog. The tiger sees the dog. The tiger visits the dog. If something likes the dog then it visits the dog. If something sees the dog and the dog is round then it likes the dog. If something visits the tiger then it visits the dog. If something is green then it visits the dog. If something visits the dog then it sees the dog. If something visits the tiger and it likes the dog then it visits the dog.
The dog is blue.
("dog" "is" "blue" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
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 is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something likes the dog then it visits the dog.
((("something" "likes" "dog" "+")) -> ("something" "visits" "dog" "+"))
If something sees the dog and the dog is round then it likes the dog.
((("something" "sees" "dog" "+") ("dog" "is" "round" "+")) -> ("something" "likes" "dog" "+"))
If something visits the tiger then it visits the dog.
((("something" "visits" "tiger" "+")) -> ("something" "visits" "dog" "+"))
If something is green then it visits the dog.
((("something" "is" "green" "+")) -> ("something" "visits" "dog" "+"))
If something visits the dog then it sees the dog.
((("something" "visits" "dog" "+")) -> ("something" "sees" "dog" "+"))
If something visits the tiger and it likes the dog then it visits the dog.
((("something" "visits" "tiger" "+") ("something" "likes" "dog" "+")) -> ("something" "visits" "dog" "+"))
The dog is green.
True
1
proof
[(triple2)]
("dog" "is" "green" "+")
triple2
The tiger is not green.
False
1
inv-proof
[(triple10)]
("tiger" "is" "green" "-")
triple10
The dog visits the dog.
True
2
proof
[(((triple2) -> rule4) OR ((triple8) -> rule3))]
("dog" "visits" "dog" "+")
((triple2) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
((triple8) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog does not visit the dog.
False
2
inv-proof
[(((triple2) -> rule4) OR ((triple8) -> rule3))]
("dog" "visits" "dog" "-")
((triple2) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
((triple8) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog sees the dog.
True
3
proof
[(((((triple2) -> rule4)) -> rule5) OR ((((triple8) -> rule3)) -> rule5))]
("dog" "sees" "dog" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog does not see the dog.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5) OR ((((triple8) -> rule3)) -> rule5))]
("dog" "sees" "dog" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog likes the dog.
True
5
proof
[(((((((triple2) -> rule4)) -> rule5) triple4) -> rule2) OR ((((((triple8) -> rule3)) -> rule5) triple4) -> rule2))]
("dog" "likes" "dog" "+")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple4) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2)) triple4) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The dog does not like the dog.
False
5
inv-proof
[(((((((triple2) -> rule4)) -> rule5) triple4) -> rule2) OR ((((((triple8) -> rule3)) -> rule5) triple4) -> rule2))]
("dog" "likes" "dog" "-")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple4) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2)) triple4) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
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 sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
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 tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
@0: The dog is blue.[(triple1)] The dog is green.[(triple2)] The dog is kind.[(triple3)] The dog is round.[(triple4)] The dog is young.[(triple5)] The dog likes the tiger.[(triple6)] The dog sees the tiger.[(triple7)] The dog visits the tiger.[(triple8)] The tiger is blue.[(triple9)] The tiger is green.[(triple10)] The tiger is kind.[(triple11)] The tiger is round.[(triple12)] The tiger likes the dog.[(triple13 OR ((triple14 triple4) -> rule2) OR ((((triple15) -> rule5) triple4) -> rule2) OR ((((((triple10) -> rule4)) -> rule5) triple4) -> rule2))] The tiger sees the dog.[(triple14 OR ((triple15) -> rule5) OR ((((triple10) -> rule4)) -> rule5) OR ((((triple13) -> rule1)) -> rule5))] The tiger visits the dog.[(triple15 OR ((triple10) -> rule4) OR ((triple13) -> rule1) OR ((((triple14 triple4) -> rule2)) -> rule1))] @1: The dog visits the dog.[(((triple2) -> rule4) OR ((triple8) -> rule3))] @2: The dog sees the dog.[(((((triple2) -> rule4)) -> rule5) OR ((((triple8) -> rule3)) -> rule5))] @3: The dog likes the dog.[(((((((triple2) -> rule4)) -> rule5) triple4) -> rule2) OR ((((((triple8) -> rule3)) -> rule5) triple4) -> rule2))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog is round.
("dog" "is" "round" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple6
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple7
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger is green.
("tiger" "is" "green" "+")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger is round.
("tiger" "is" "round" "+")
triple12
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple13
((triple14 triple4) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
((((triple15) -> (rule5 % int2)) triple4) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
((((((triple10) -> (rule4 % int3))) -> (rule5 % int2)) triple4) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple14
((triple15) -> (rule5 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
((((triple13) -> (rule1 % int2))) -> (rule5 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple15
((triple10) -> (rule4 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
((triple13) -> (rule1 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
((((triple14 triple4) -> (rule2 % int2))) -> (rule1 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple2) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
((triple8) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple4) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2)) triple4) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3