The cat is big. The dog sees the rabbit. The rabbit visits the dog. If something visits the dog then the dog is cold.
The cat is big.
("cat" "is" "big" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If something visits the dog then the dog is cold.
((("something" "visits" "dog" "+")) -> ("dog" "is" "cold" "+"))
The dog sees the rabbit.
True
1
proof
[(triple2)]
("dog" "sees" "rabbit" "+")
triple2
The dog does not see the rabbit.
False
1
inv-proof
[(triple2)]
("dog" "sees" "rabbit" "-")
triple2
The dog is cold.
True
2
proof
[(((triple3) -> rule1))]
("dog" "is" "cold" "+")
((triple3) -> (rule1 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is not cold.
False
2
inv-proof
[(((triple3) -> rule1))]
("dog" "is" "cold" "-")
((triple3) -> (rule1 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog does not chase the cat.
Unknown
inv-random
[@0: The dog chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "cat" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat sees the dog.
Unknown
random
[@0: The cat sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "dog" "+")
@0: The cat is big.[(triple1)] The dog sees the rabbit.[(triple2)] The rabbit visits the dog.[(triple3)] @1: The dog is cold.[(((triple3) -> rule1))]
The cat is big.
("cat" "is" "big" "+")
triple1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple2
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple3
The dog is cold.
("dog" "is" "cold" "+")
((triple3) -> (rule1 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1