The dog is cold. The dog visits the tiger. The tiger is blue. If something is big and not rough then it visits the tiger. If something sees the tiger then it does not see the dog. If the dog does not visit the tiger then the dog is not blue. If something is blue and it does not chase the dog then it sees the tiger. If something is blue then it sees the tiger. If something is kind then it sees the tiger.
The dog is cold.
("dog" "is" "cold" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If something is big and not rough then it visits the tiger.
((("something" "is" "big" "+") ("something" "is" "rough" "~")) -> ("something" "visits" "tiger" "+"))
If something sees the tiger then it does not see the dog.
((("something" "sees" "tiger" "+")) -> ("something" "sees" "dog" "-"))
If the dog does not visit the tiger then the dog is not blue.
((("dog" "visits" "tiger" "~")) -> ("dog" "is" "blue" "-"))
If something is blue and it does not chase the dog then it sees the tiger.
((("something" "is" "blue" "+") ("something" "chases" "dog" "~")) -> ("something" "sees" "tiger" "+"))
If something is blue then it sees the tiger.
((("something" "is" "blue" "+")) -> ("something" "sees" "tiger" "+"))
If something is kind then it sees the tiger.
((("something" "is" "kind" "+")) -> ("something" "sees" "tiger" "+"))
The dog visits the tiger.
True
1
proof
[(triple2)]
("dog" "visits" "tiger" "+")
triple2
The tiger is not blue.
False
1
inv-proof
[(triple3)]
("tiger" "is" "blue" "-")
triple3
The tiger sees the tiger.
True
2
proof
[(((triple3) -> rule5))]
("tiger" "sees" "tiger" "+")
((triple3) -> (rule5 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger does not see the tiger.
False
2
inv-proof
[(((triple3) -> rule5))]
("tiger" "sees" "tiger" "-")
((triple3) -> (rule5 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger does not see the dog.
True
3
proof
[(((((triple3) -> rule5)) -> rule2))]
("tiger" "sees" "dog" "-")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger sees the dog.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule2))]
("tiger" "sees" "dog" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The dog sees the tiger.
Unknown
rconc
[@1: The dog sees the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "sees" "tiger" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The dog is cold.[(triple1)] The dog visits the tiger.[(triple2)] The tiger is blue.[(triple3)] @1: The tiger sees the tiger.[(((triple3) -> rule5))] @2: The tiger does not see the dog.[(((((triple3) -> rule5)) -> rule2))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple2
The tiger is blue.
("tiger" "is" "blue" "+")
triple3
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple3) -> (rule5 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2