The cow is round. The dog likes the squirrel. The squirrel is kind. Round things are cold. If something is cold then it visits the cow. If something needs the squirrel and it does not like the dog then the dog does not like the cow. If something is young and it needs the dog then it needs the squirrel. If something visits the squirrel then the squirrel likes the cow. If something visits the dog then the dog is not kind.
The cow is round.
("cow" "is" "round" "+")
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
Round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it visits the cow.
((("something" "is" "cold" "+")) -> ("something" "visits" "cow" "+"))
If something needs the squirrel and it does not like the dog then the dog does not like the cow.
((("something" "needs" "squirrel" "+") ("something" "likes" "dog" "~")) -> ("dog" "likes" "cow" "-"))
If something is young and it needs the dog then it needs the squirrel.
((("something" "is" "young" "+") ("something" "needs" "dog" "+")) -> ("something" "needs" "squirrel" "+"))
If something visits the squirrel then the squirrel likes the cow.
((("something" "visits" "squirrel" "+")) -> ("squirrel" "likes" "cow" "+"))
If something visits the dog then the dog is not kind.
((("something" "visits" "dog" "+")) -> ("dog" "is" "kind" "-"))
The cow is round.
True
1
proof
[(triple1)]
("cow" "is" "round" "+")
triple1
The squirrel is not kind.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "kind" "-")
triple3
The cow is cold.
True
2
proof
[(((triple1) -> rule1))]
("cow" "is" "cold" "+")
((triple1) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is not cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("cow" "is" "cold" "-")
((triple1) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow visits the cow.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("cow" "visits" "cow" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow does not visit the cow.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("cow" "visits" "cow" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The dog is not cold.
Unknown
inv-rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "cold" "-")
The cow needs the squirrel.
Unknown
rconc
[@1: The cow needs the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "needs" "squirrel" "+")
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The cow visits the squirrel.
Unknown
random
[@0: The cow visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "squirrel" "+")
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
@0: The cow is round.[(triple1)] The dog likes the squirrel.[(triple2)] The squirrel is kind.[(triple3)] @1: The cow is cold.[(((triple1) -> rule1))] @2: The cow visits the cow.[(((((triple1) -> rule1)) -> rule2))]
The cow is round.
("cow" "is" "round" "+")
triple1
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple2
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple3
The cow is cold.
("cow" "is" "cold" "+")
((triple1) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2