Anne is big. Erin is quiet. Gary is nice. Harry is nice. If something is big and nice then it is white. If Harry is nice then Harry is big. If Anne is red and Anne is not kind then Anne is big. Kind, red things are big. All nice, quiet things are not big. Quiet things are not big. Nice, young things are red. White things are not quiet.
Anne is big.
("Anne" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If something is big and nice then it is white.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If Harry is nice then Harry is big.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "big" "+"))
If Anne is red and Anne is not kind then Anne is big.
((("Anne" "is" "red" "+") ("Anne" "is" "kind" "~")) -> ("Anne" "is" "big" "+"))
Kind, red things are big.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
All nice, quiet things are not big.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "-"))
Quiet things are not big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "-"))
Nice, young things are red.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
White things are not quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "-"))
Erin is quiet.
True
1
proof
[(triple2)]
("Erin" "is" "quiet" "+")
triple2
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Harry is big.
True
2
proof
[(((triple4) -> rule2))]
("Harry" "is" "big" "+")
((triple4) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Erin is big.
False
2
inv-proof
[(((triple2) -> rule6))]
("Erin" "is" "big" "+")
((triple2) -> (rule6 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Harry is white.
True
4
proof
[(((((triple4) -> rule2) triple4) -> rule1))]
("Harry" "is" "white" "+")
((((triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not white.
False
4
inv-proof
[(((((triple4) -> rule2) triple4) -> rule1))]
("Harry" "is" "white" "-")
((((triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not quiet.
True
5
proof
[(((((((triple4) -> rule2) triple4) -> rule1)) -> rule8))]
("Harry" "is" "quiet" "-")
((((((triple4) -> (rule2 % int3)) triple4) -> (rule1 % int2))) -> (rule8 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is quiet.
False
5
inv-proof
[(((((((triple4) -> rule2) triple4) -> rule1)) -> rule8))]
("Harry" "is" "quiet" "+")
((((((triple4) -> (rule2 % int3)) triple4) -> (rule1 % int2))) -> (rule8 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "red" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "big" "+")
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "white" "-")
Gary is white.
Unknown
rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Gary" "is" "white" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Anne is big.[(triple1)] Erin is quiet.[(triple2)] Gary is nice.[(triple3)] Harry is nice.[(triple4)] @1: Erin is not big.[(((triple2) -> rule6))] Harry is big.[(((triple4) -> rule2))] @2: Harry is white.[(((((triple4) -> rule2) triple4) -> rule1))] @3: Harry is not quiet.[(((((((triple4) -> rule2) triple4) -> rule1)) -> rule8))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Erin is not big.
("Erin" "is" "big" "-")
((triple2) -> (rule6 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple4) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((((triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not quiet.
("Harry" "is" "quiet" "-")
((((((triple4) -> (rule2 % int3)) triple4) -> (rule1 % int2))) -> (rule8 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3