The dog is round. The squirrel visits the dog. The tiger likes the dog. If someone likes the dog then the dog visits the tiger. If someone likes the squirrel and they need the squirrel then they do not like the dog. If someone needs the dog then the dog needs the squirrel. If someone visits the tiger then the tiger does not need the dog. If the dog is not rough then the dog is not round. If someone likes the dog and they do not need the dog then the dog is cold.
The dog is round.
("dog" "is" "round" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
If someone likes the dog then the dog visits the tiger.
((("someone" "likes" "dog" "+")) -> ("dog" "visits" "tiger" "+"))
If someone likes the squirrel and they need the squirrel then they do not like the dog.
((("someone" "likes" "squirrel" "+") ("someone" "needs" "squirrel" "+")) -> ("someone" "likes" "dog" "-"))
If someone needs the dog then the dog needs the squirrel.
((("someone" "needs" "dog" "+")) -> ("dog" "needs" "squirrel" "+"))
If someone visits the tiger then the tiger does not need the dog.
((("someone" "visits" "tiger" "+")) -> ("tiger" "needs" "dog" "-"))
If the dog is not rough then the dog is not round.
((("dog" "is" "rough" "~")) -> ("dog" "is" "round" "-"))
If someone likes the dog and they do not need the dog then the dog is cold.
((("someone" "likes" "dog" "+") ("someone" "needs" "dog" "~")) -> ("dog" "is" "cold" "+"))
The dog is round.
True
1
proof
[(triple1)]
("dog" "is" "round" "+")
triple1
The tiger does not like the dog.
False
1
inv-proof
[(triple3)]
("tiger" "likes" "dog" "-")
triple3
The dog visits the tiger.
True
2
proof
[(((triple3) -> rule1))]
("dog" "visits" "tiger" "+")
((triple3) -> (rule1 % int1))
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int1
The dog does not visit the tiger.
False
2
inv-proof
[(((triple3) -> rule1))]
("dog" "visits" "tiger" "-")
((triple3) -> (rule1 % int1))
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int1
The tiger does not need the dog.
True
3
proof
[(((((triple3) -> rule1)) -> rule4))]
("tiger" "needs" "dog" "-")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The tiger does not need the dog.
("tiger" "needs" "dog" "-")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int2
The tiger needs the dog.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule4))]
("tiger" "needs" "dog" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The tiger does not need the dog.
("tiger" "needs" "dog" "-")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int2
The dog is cold.
True
5
proof
[(((triple3 ((((triple3) -> rule1)) -> rule4)) -> rule6))]
("dog" "is" "cold" "+")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The tiger does not need the dog.
("tiger" "needs" "dog" "-")
int2
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int3
The dog is not cold.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule1)) -> rule4)) -> rule6))]
("dog" "is" "cold" "-")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The tiger does not need the dog.
("tiger" "needs" "dog" "-")
int2
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int3
The dog does not need the squirrel.
Unknown
inv-rconc
[@1: The dog needs the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "needs" "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 does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The dog needs the tiger.
Unknown
random
[@0: The dog needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "tiger" "+")
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
@0: The dog is round.[(triple1)] The squirrel visits the dog.[(triple2)] The tiger likes the dog.[(triple3)] @1: The dog visits the tiger.[(((triple3) -> rule1))] @2: The tiger does not need the dog.[(((((triple3) -> rule1)) -> rule4))] @3: The dog is cold.[(((triple3 ((((triple3) -> rule1)) -> rule4)) -> rule6))]
The dog is round.
("dog" "is" "round" "+")
triple1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple3
The dog visits the tiger.
("dog" "visits" "tiger" "+")
((triple3) -> (rule1 % int1))
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int1
The tiger does not need the dog.
("tiger" "needs" "dog" "-")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The tiger does not need the dog.
("tiger" "needs" "dog" "-")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The tiger does not need the dog.
("tiger" "needs" "dog" "-")
int2
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int3