The dog does not chase the squirrel. The squirrel chases the dog. The squirrel is kind. If someone needs the dog then the dog chases the squirrel. If someone needs the dog then the dog does not chase the squirrel. If someone visits the dog and they are nice then they visit the squirrel. All rough people are cold. If someone needs the dog then the dog is not nice. If someone visits the dog then they do not chase the squirrel. If someone chases the dog then the dog does not need the squirrel. If the dog does not need the squirrel then the squirrel is cold.
The dog does not chase the squirrel.
("dog" "chases" "squirrel" "-")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
If someone needs the dog then the dog chases the squirrel.
((("someone" "needs" "dog" "+")) -> ("dog" "chases" "squirrel" "+"))
If someone needs the dog then the dog does not chase the squirrel.
((("someone" "needs" "dog" "+")) -> ("dog" "chases" "squirrel" "-"))
If someone visits the dog and they are nice then they visit the squirrel.
((("someone" "visits" "dog" "+") ("someone" "is" "nice" "+")) -> ("someone" "visits" "squirrel" "+"))
All rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone needs the dog then the dog is not nice.
((("someone" "needs" "dog" "+")) -> ("dog" "is" "nice" "-"))
If someone visits the dog then they do not chase the squirrel.
((("someone" "visits" "dog" "+")) -> ("someone" "chases" "squirrel" "-"))
If someone chases the dog then the dog does not need the squirrel.
((("someone" "chases" "dog" "+")) -> ("dog" "needs" "squirrel" "-"))
If the dog does not need the squirrel then the squirrel is cold.
((("dog" "needs" "squirrel" "~")) -> ("squirrel" "is" "cold" "+"))
The squirrel chases the dog.
True
1
proof
[(triple2)]
("squirrel" "chases" "dog" "+")
triple2
The dog chases the squirrel.
False
1
inv-proof
[(triple1)]
("dog" "chases" "squirrel" "+")
triple1
The dog does not need the squirrel.
True
2
proof
[(((triple2) -> rule7))]
("dog" "needs" "squirrel" "-")
((triple2) -> (rule7 % int1))
The dog does not need the squirrel.
("dog" "needs" "squirrel" "-")
int1
The dog needs the squirrel.
False
2
inv-proof
[(((triple2) -> rule7))]
("dog" "needs" "squirrel" "+")
((triple2) -> (rule7 % int1))
The dog does not need the squirrel.
("dog" "needs" "squirrel" "-")
int1
The squirrel is cold.
True
3
proof
[(((((triple2) -> rule7)) -> rule8))]
("squirrel" "is" "cold" "+")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The dog does not need the squirrel.
("dog" "needs" "squirrel" "-")
int2
The squirrel is not cold.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule8))]
("squirrel" "is" "cold" "-")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The dog does not need the squirrel.
("dog" "needs" "squirrel" "-")
int2
The dog is not cold.
Unknown
inv-rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "cold" "-")
The dog visits the squirrel.
Unknown
rconc
[@1: The dog visits the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "visits" "squirrel" "+")
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
@0: The dog does not chase the squirrel.[(triple1)] The squirrel chases the dog.[(triple2)] The squirrel is kind.[(triple3)] @1: The dog does not need the squirrel.[(((triple2) -> rule7))] @2: The squirrel is cold.[(((((triple2) -> rule7)) -> rule8))]
The dog does not chase the squirrel.
("dog" "chases" "squirrel" "-")
triple1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple2
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple3
The dog does not need the squirrel.
("dog" "needs" "squirrel" "-")
((triple2) -> (rule7 % int1))
The dog does not need the squirrel.
("dog" "needs" "squirrel" "-")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The dog does not need the squirrel.
("dog" "needs" "squirrel" "-")
int2