Anne is kind. Anne is red. Erin is red. Erin is round. Erin is young. Gary is quiet. Harry is big. Harry is green. Harry is quiet. Harry is round. If Gary is quiet then Gary is green. Quiet people are kind. Green people are young. All young people are big. If someone is green then they are young. If Anne is round and Anne is young then Anne is red.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
If Gary is quiet then Gary is green.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "green" "+"))
Quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
All young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is green then they are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If Anne is round and Anne is young then Anne is red.
((("Anne" "is" "round" "+") ("Anne" "is" "young" "+")) -> ("Anne" "is" "red" "+"))
Gary is quiet.
True
1
proof
[(triple6)]
("Gary" "is" "quiet" "+")
triple6
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Harry is kind.
True
2
proof
[(((triple9) -> rule2))]
("Harry" "is" "kind" "+")
((triple9) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple5) -> rule4))]
("Erin" "is" "big" "-")
((triple5) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Gary is young.
True
3
proof
[(((((triple6) -> rule1)) -> rule3) OR ((((triple6) -> rule1)) -> rule5))]
("Gary" "is" "young" "+")
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not young.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule3) OR ((((triple6) -> rule1)) -> rule5))]
("Gary" "is" "young" "-")
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
True
4
proof
[(((((((triple6) -> rule1)) -> rule3)) -> rule4) OR ((((((triple6) -> rule1)) -> rule5)) -> rule4))]
("Gary" "is" "big" "+")
((((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((((triple6) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not big.
False
4
inv-proof
[(((((((triple6) -> rule1)) -> rule3)) -> rule4) OR ((((((triple6) -> rule1)) -> rule5)) -> rule4))]
("Gary" "is" "big" "-")
((((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((((triple6) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "young" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "kind" "+")
Anne is not big.
Unknown
inv-rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Anne is kind.[(triple1)] Anne is red.[(triple2)] Erin is red.[(triple3)] Erin is round.[(triple4)] Erin is young.[(triple5)] Gary is quiet.[(triple6)] Harry is big.[(triple7 OR ((((triple8) -> rule3)) -> rule4) OR ((((triple8) -> rule5)) -> rule4))] Harry is green.[(triple8)] Harry is quiet.[(triple9)] Harry is round.[(triple10)] @1: Erin is big.[(((triple5) -> rule4))] Gary is green.[(((triple6) -> rule1))] Gary is kind.[(((triple6) -> rule2))] Harry is kind.[(((triple9) -> rule2))] Harry is young.[(((triple8) -> rule3) OR ((triple8) -> rule5))] @2: Gary is young.[(((((triple6) -> rule1)) -> rule3) OR ((((triple6) -> rule1)) -> rule5))] @3: Gary is big.[(((((((triple6) -> rule1)) -> rule3)) -> rule4) OR ((((((triple6) -> rule1)) -> rule5)) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
((((triple8) -> (rule3 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
Erin is big.
("Erin" "is" "big" "+")
((triple5) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple6) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple6) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple9) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple8) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple8) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((((triple6) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3