The dog chases the tiger. The dog sees the tiger. The tiger chases the dog. The tiger is big. The tiger is round. The tiger sees the dog. The tiger visits the dog. If something is cold and it sees the tiger then the tiger chases the dog. If something chases the dog then it visits the dog. If something sees the tiger then it visits the tiger. If the dog sees the tiger then the tiger visits the dog. If something chases the dog then it is cold. All big, round things are cold.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something is cold and it sees the tiger then the tiger chases the dog.
((("something" "is" "cold" "+") ("something" "sees" "tiger" "+")) -> ("tiger" "chases" "dog" "+"))
If something chases the dog then it visits the dog.
((("something" "chases" "dog" "+")) -> ("something" "visits" "dog" "+"))
If something sees the tiger then it visits the tiger.
((("something" "sees" "tiger" "+")) -> ("something" "visits" "tiger" "+"))
If the dog sees the tiger then the tiger visits the dog.
((("dog" "sees" "tiger" "+")) -> ("tiger" "visits" "dog" "+"))
If something chases the dog then it is cold.
((("something" "chases" "dog" "+")) -> ("something" "is" "cold" "+"))
All big, round things are cold.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
The dog sees the tiger.
True
1
proof
[(triple2)]
("dog" "sees" "tiger" "+")
triple2
The tiger does not visit the dog.
False
1
inv-proof
[(triple7 OR ((triple2) -> rule4) OR ((triple3) -> rule2))]
("tiger" "visits" "dog" "-")
triple7
((triple2) -> (rule4 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
((triple3) -> (rule2 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger is cold.
True
2
proof
[(((triple3) -> rule5) OR ((triple4 triple5) -> rule6))]
("tiger" "is" "cold" "+")
((triple3) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
((triple4 triple5) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The dog does not visit the tiger.
False
2
inv-proof
[(((triple2) -> rule3))]
("dog" "visits" "tiger" "-")
((triple2) -> (rule3 % int1))
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int1
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The dog visits the dog.
Unknown
rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "visits" "dog" "+")
The tiger is not red.
Unknown
inv-random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog chases the tiger.[(triple1)] The dog sees the tiger.[(triple2)] The tiger chases the dog.[(triple3)] The tiger is big.[(triple4)] The tiger is round.[(triple5)] The tiger sees the dog.[(triple6)] The tiger visits the dog.[(triple7 OR ((triple2) -> rule4) OR ((triple3) -> rule2))] @1: The dog visits the tiger.[(((triple2) -> rule3))] The tiger is cold.[(((triple3) -> rule5) OR ((triple4 triple5) -> rule6))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple2
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple3
The tiger is big.
("tiger" "is" "big" "+")
triple4
The tiger is round.
("tiger" "is" "round" "+")
triple5
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple6
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple7
((triple2) -> (rule4 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
((triple3) -> (rule2 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
((triple2) -> (rule3 % int1))
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((triple3) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
((triple4 triple5) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1