The cow is young. The squirrel does not need the cow. If someone sees the cow and they need the squirrel then they are kind. If the cow is kind then the cow needs the squirrel. If the squirrel sees the cow and the squirrel is not young then the cow needs the squirrel. If someone is round and they see the cow then the cow does not see the squirrel. If someone is round then they eat the squirrel. If someone eats the squirrel then the squirrel is round. Young people are round. If the cow does not need the squirrel then the squirrel is cold.
The cow is young.
("cow" "is" "young" "+")
The squirrel does not need the cow.
("squirrel" "needs" "cow" "-")
If someone sees the cow and they need the squirrel then they are kind.
((("someone" "sees" "cow" "+") ("someone" "needs" "squirrel" "+")) -> ("someone" "is" "kind" "+"))
If the cow is kind then the cow needs the squirrel.
((("cow" "is" "kind" "+")) -> ("cow" "needs" "squirrel" "+"))
If the squirrel sees the cow and the squirrel is not young then the cow needs the squirrel.
((("squirrel" "sees" "cow" "+") ("squirrel" "is" "young" "~")) -> ("cow" "needs" "squirrel" "+"))
If someone is round and they see the cow then the cow does not see the squirrel.
((("someone" "is" "round" "+") ("someone" "sees" "cow" "+")) -> ("cow" "sees" "squirrel" "-"))
If someone is round then they eat the squirrel.
((("someone" "is" "round" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone eats the squirrel then the squirrel is round.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "is" "round" "+"))
Young people are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If the cow does not need the squirrel then the squirrel is cold.
((("cow" "needs" "squirrel" "~")) -> ("squirrel" "is" "cold" "+"))
The squirrel does not need the cow.
True
1
proof
[(triple2)]
("squirrel" "needs" "cow" "-")
triple2
The squirrel needs the cow.
False
1
inv-proof
[(triple2)]
("squirrel" "needs" "cow" "+")
triple2
The cow is round.
True
2
proof
[(((triple1) -> rule7))]
("cow" "is" "round" "+")
((triple1) -> (rule7 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is not round.
False
2
inv-proof
[(((triple1) -> rule7))]
("cow" "is" "round" "-")
((triple1) -> (rule7 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow eats the squirrel.
True
3
proof
[(((((triple1) -> rule7)) -> rule5))]
("cow" "eats" "squirrel" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow does not eat the squirrel.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule5))]
("cow" "eats" "squirrel" "-")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The squirrel is round.
True
4
proof
[(((((((triple1) -> rule7)) -> rule5)) -> rule6))]
("squirrel" "is" "round" "+")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The squirrel is not round.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule5)) -> rule6))]
("squirrel" "is" "round" "-")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The cow does not need the squirrel.
Unknown
inv-rconc
[@2: The cow needs the squirrel.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("cow" "needs" "squirrel" "-")
The squirrel is cold.
Unknown
rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "is" "cold" "+")
The squirrel is not kind.
Unknown
inv-rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "kind" "-")
The cow is kind.
Unknown
rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "kind" "+")
The squirrel does not see the cow.
Unknown
inv-random
[@0: The squirrel sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "cow" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
@0: The cow is young.[(triple1)] The squirrel does not need the cow.[(triple2)] @1: The cow is round.[(((triple1) -> rule7))] @2: The cow eats the squirrel.[(((((triple1) -> rule7)) -> rule5))] @3: The squirrel is round.[(((((((triple1) -> rule7)) -> rule5)) -> rule6))] @4: The squirrel eats the squirrel.[(((((((((triple1) -> rule7)) -> rule5)) -> rule6)) -> rule5))]
The cow is young.
("cow" "is" "young" "+")
triple1
The squirrel does not need the cow.
("squirrel" "needs" "cow" "-")
triple2
The cow is round.
("cow" "is" "round" "+")
((triple1) -> (rule7 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int3
The cow is round.
("cow" "is" "round" "+")
int4