The cow is young. Kind things are red. If something is nice then it is red. All red things are kind. If something is red then it is kind. If the cow is young then the cow is nice. If the cow is young then the cow is nice. Red, young things are nice. If something is nice and not red then it is round.
The cow is young.
("cow" "is" "young" "+")
Kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is red then it is kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If the cow is young then the cow is nice.
((("cow" "is" "young" "+")) -> ("cow" "is" "nice" "+"))
If the cow is young then the cow is nice.
((("cow" "is" "young" "+")) -> ("cow" "is" "nice" "+"))
Red, young things are nice.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is nice and not red then it is round.
((("something" "is" "nice" "+") ("something" "is" "red" "~")) -> ("something" "is" "round" "+"))
The cow is young.
True
1
proof
[(triple1)]
("cow" "is" "young" "+")
triple1
The cow is not young.
False
1
inv-proof
[(triple1)]
("cow" "is" "young" "-")
triple1
The cow is nice.
True
2
proof
[(((triple1) -> rule5) OR ((triple1) -> rule6))]
("cow" "is" "nice" "+")
((triple1) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
((triple1) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is not nice.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple1) -> rule6))]
("cow" "is" "nice" "-")
((triple1) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
((triple1) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is red.
True
3
proof
[(((((triple1) -> rule5)) -> rule2) OR ((((triple1) -> rule6)) -> rule2))]
("cow" "is" "red" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is not red.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule2) OR ((((triple1) -> rule6)) -> rule2))]
("cow" "is" "red" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is kind.
True
4
proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule3) OR ((((((triple1) -> rule5)) -> rule2)) -> rule4) OR ((((((triple1) -> rule6)) -> rule2)) -> rule3) OR ((((((triple1) -> rule6)) -> rule2)) -> rule4))]
("cow" "is" "kind" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The cow is not kind.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule3) OR ((((((triple1) -> rule5)) -> rule2)) -> rule4) OR ((((((triple1) -> rule6)) -> rule2)) -> rule3) OR ((((((triple1) -> rule6)) -> rule2)) -> rule4))]
("cow" "is" "kind" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The cow is not round.
Unknown
inv-rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "is" "round" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow is young.[(triple1)] @1: The cow is nice.[(((triple1) -> rule5) OR ((triple1) -> rule6))] @2: The cow is red.[(((((triple1) -> rule5)) -> rule2) OR ((((triple1) -> rule6)) -> rule2))] @3: The cow is kind.[(((((((triple1) -> rule5)) -> rule2)) -> rule3) OR ((((((triple1) -> rule5)) -> rule2)) -> rule4) OR ((((((triple1) -> rule6)) -> rule2)) -> rule3) OR ((((((triple1) -> rule6)) -> rule2)) -> rule4))]
The cow is young.
("cow" "is" "young" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
((triple1) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
((triple1) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is red.
("cow" "is" "red" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3