The dog eats the tiger. The dog is big. The tiger chases the dog. If the tiger visits the dog then the dog chases the tiger. If someone visits the tiger and the tiger chases the dog then they are cold. If someone chases the dog then they visit the tiger.
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is big.
("dog" "is" "big" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
If the tiger visits the dog then the dog chases the tiger.
((("tiger" "visits" "dog" "+")) -> ("dog" "chases" "tiger" "+"))
If someone visits the tiger and the tiger chases the dog then they are cold.
((("someone" "visits" "tiger" "+") ("tiger" "chases" "dog" "+")) -> ("someone" "is" "cold" "+"))
If someone chases the dog then they visit the tiger.
((("someone" "chases" "dog" "+")) -> ("someone" "visits" "tiger" "+"))
The tiger chases the dog.
True
1
proof
[(triple3)]
("tiger" "chases" "dog" "+")
triple3
The dog is not big.
False
1
inv-proof
[(triple2)]
("dog" "is" "big" "-")
triple2
The tiger visits the tiger.
True
2
proof
[(((triple3) -> rule3))]
("tiger" "visits" "tiger" "+")
((triple3) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger does not visit the tiger.
False
2
inv-proof
[(((triple3) -> rule3))]
("tiger" "visits" "tiger" "-")
((triple3) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is cold.
True
4
proof
[(((((triple3) -> rule3) triple3) -> rule2))]
("tiger" "is" "cold" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger is not cold.
False
4
inv-proof
[(((((triple3) -> rule3) triple3) -> rule2))]
("tiger" "is" "cold" "-")
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The dog is not cold.
Unknown
inv-rconc
[@2: The dog is cold.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("dog" "is" "cold" "-")
The dog chases the tiger.
Unknown
rconc
[@1: The dog chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "tiger" "+")
The dog does not visit the tiger.
Unknown
inv-rconc
[@1: The dog visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "visits" "tiger" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The dog eats the tiger.[(triple1)] The dog is big.[(triple2)] The tiger chases the dog.[(triple3)] @1: The tiger visits the tiger.[(((triple3) -> rule3))] @2: The tiger is cold.[(((((triple3) -> rule3) triple3) -> rule2))]
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple3) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2