The dog chases the tiger. The dog is big. The dog is cold. The dog is green. The dog visits the tiger. The tiger is big. The tiger is green. The tiger is round. The tiger sees the dog. The tiger visits the dog. If someone sees the tiger then they are big. If someone sees the tiger then the tiger chases the dog. If the dog chases the tiger then the tiger is green. If someone is big and they visit the tiger then they see the tiger. If someone chases the tiger and the tiger is cold then they are green. If someone visits the tiger then the tiger sees the dog.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If someone sees the tiger then they are big.
((("someone" "sees" "tiger" "+")) -> ("someone" "is" "big" "+"))
If someone sees the tiger then the tiger chases the dog.
((("someone" "sees" "tiger" "+")) -> ("tiger" "chases" "dog" "+"))
If the dog chases the tiger then the tiger is green.
((("dog" "chases" "tiger" "+")) -> ("tiger" "is" "green" "+"))
If someone is big and they visit the tiger then they see the tiger.
((("someone" "is" "big" "+") ("someone" "visits" "tiger" "+")) -> ("someone" "sees" "tiger" "+"))
If someone chases the tiger and the tiger is cold then they are green.
((("someone" "chases" "tiger" "+") ("tiger" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone visits the tiger then the tiger sees the dog.
((("someone" "visits" "tiger" "+")) -> ("tiger" "sees" "dog" "+"))
The dog is big.
True
1
proof
[(triple2)]
("dog" "is" "big" "+")
triple2
The tiger is not green.
False
1
inv-proof
[(triple7 OR ((triple1) -> rule3))]
("tiger" "is" "green" "-")
triple7
((triple1) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The dog sees the tiger.
True
3
proof
[(((triple2 triple5) -> rule4))]
("dog" "sees" "tiger" "+")
((triple2 triple5) -> (rule4 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The dog does not see the tiger.
False
3
inv-proof
[(((triple2 triple5) -> rule4))]
("dog" "sees" "tiger" "-")
((triple2 triple5) -> (rule4 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The tiger chases the dog.
True
4
proof
[(((((triple2 triple5) -> rule4)) -> rule2))]
("tiger" "chases" "dog" "+")
((((triple2 triple5) -> (rule4 % int2))) -> (rule2 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int2
The tiger does not chase the dog.
False
4
inv-proof
[(((((triple2 triple5) -> rule4)) -> rule2))]
("tiger" "chases" "dog" "-")
((((triple2 triple5) -> (rule4 % int2))) -> (rule2 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int2
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
The tiger is not blue.
Unknown
inv-random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The dog chases the tiger.[(triple1)] The dog is big.[(triple2)] The dog is cold.[(triple3)] The dog is green.[(triple4)] The dog visits the tiger.[(triple5)] The tiger is big.[(triple6)] The tiger is green.[(triple7 OR ((triple1) -> rule3))] The tiger is round.[(triple8)] The tiger sees the dog.[(triple9 OR ((triple5) -> rule6))] The tiger visits the dog.[(triple10)] @1: The dog sees the tiger.[(((triple2 triple5) -> rule4))] @2: The tiger chases the dog.[(((((triple2 triple5) -> rule4)) -> rule2))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is green.
("dog" "is" "green" "+")
triple4
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple5
The tiger is big.
("tiger" "is" "big" "+")
triple6
The tiger is green.
("tiger" "is" "green" "+")
triple7
((triple1) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
triple8
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple9
((triple5) -> (rule6 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple10
The dog sees the tiger.
("dog" "sees" "tiger" "+")
((triple2 triple5) -> (rule4 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
((((triple2 triple5) -> (rule4 % int2))) -> (rule2 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int2