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