Anne is big. Anne is green. Erin is young. Gary is furry. Gary is round. Gary is young. Harry is young. If something is green then it is not furry. Young things are white. All round things are big. If something is white then it is big. If something is white then it is nice. If something is big then it is young.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is green then it is not furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "-"))
Young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something is white then it is big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is white then it is nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is big then it is young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Gary is furry.
True
1
proof
[(triple4)]
("Gary" "is" "furry" "+")
triple4
Erin is not young.
False
1
inv-proof
[(triple3)]
("Erin" "is" "young" "-")
triple3
Anne is young.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "young" "+")
((triple1) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple6) -> rule2) OR ((((((triple5) -> rule3)) -> rule6)) -> rule2))]
("Gary" "is" "white" "-")
((triple6) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Harry is big.
True
3
proof
[(((((triple7) -> rule2)) -> rule4))]
("Harry" "is" "big" "+")
((((triple7) -> (rule2 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Gary is not nice.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule5) OR ((((((((triple5) -> rule3)) -> rule6)) -> rule2)) -> rule5))]
("Gary" "is" "nice" "-")
((((triple6) -> (rule2 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((((((triple5) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Anne is nice.
True
4
proof
[(((((((triple1) -> rule6)) -> rule2)) -> rule5))]
("Anne" "is" "nice" "+")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not nice.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule2)) -> rule5))]
("Anne" "is" "nice" "-")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2)] Erin is young.[(triple3)] Gary is furry.[(triple4)] Gary is round.[(triple5)] Gary is young.[(triple6 OR ((((triple5) -> rule3)) -> rule6))] Harry is young.[(triple7)] @1: Anne is not furry.[(((triple2) -> rule1))] Anne is young.[(((triple1) -> rule6))] Erin is white.[(((triple3) -> rule2))] Gary is big.[(((triple5) -> rule3) OR ((((triple6) -> rule2)) -> rule4))] Gary is white.[(((triple6) -> rule2) OR ((((((triple5) -> rule3)) -> rule6)) -> rule2))] Harry is white.[(((triple7) -> rule2))] @2: Anne is white.[(((((triple1) -> rule6)) -> rule2))] Erin is big.[(((((triple3) -> rule2)) -> rule4))] Erin is nice.[(((((triple3) -> rule2)) -> rule5))] Gary is nice.[(((((triple6) -> rule2)) -> rule5) OR ((((((((triple5) -> rule3)) -> rule6)) -> rule2)) -> rule5))] Harry is big.[(((((triple7) -> rule2)) -> rule4))] Harry is nice.[(((((triple7) -> rule2)) -> rule5))] @3: Anne is nice.[(((((((triple1) -> rule6)) -> rule2)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
Gary is round.
("Gary" "is" "round" "+")
triple5
Gary is young.
("Gary" "is" "young" "+")
triple6
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple7
Anne is not furry.
("Anne" "is" "furry" "-")
((triple2) -> (rule1 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple3) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple5) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple6) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((triple7) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple6) -> (rule2 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((((((triple5) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
((((triple7) -> (rule2 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3