Erin is green. Erin is round. Erin is smart. Gary is green. Gary is kind. Gary is not nice. Gary is quiet. If something is rough then it is smart. If something is quiet then it is smart. If something is rough and nice then it is quiet. If Gary is quiet then Gary is not nice. If something is smart and kind then it is rough. All kind, rough things are not nice. If Gary is rough then Gary is round. Quiet, kind things are green.
Erin is green.
("Erin" "is" "green" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not nice.
("Gary" "is" "nice" "-")
Gary is quiet.
("Gary" "is" "quiet" "+")
If something is rough then it is smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is quiet then it is smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If something is rough and nice then it is quiet.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If Gary is quiet then Gary is not nice.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "nice" "-"))
If something is smart and kind then it is rough.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
All kind, rough things are not nice.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "-"))
If Gary is rough then Gary is round.
((("Gary" "is" "rough" "+")) -> ("Gary" "is" "round" "+"))
Quiet, kind things are green.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Erin is smart.
True
1
proof
[(triple3)]
("Erin" "is" "smart" "+")
triple3
Erin is not smart.
False
1
inv-proof
[(triple3)]
("Erin" "is" "smart" "-")
triple3
Gary is smart.
True
2
proof
[(((triple7) -> rule2))]
("Gary" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple7) -> rule2))]
("Gary" "is" "smart" "-")
((triple7) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
True
4
proof
[(((((triple7) -> rule2) triple5) -> rule5))]
("Gary" "is" "rough" "+")
((((triple7) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not rough.
False
4
inv-proof
[(((((triple7) -> rule2) triple5) -> rule5))]
("Gary" "is" "rough" "-")
((((triple7) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
True
5
proof
[(((((((triple7) -> rule2) triple5) -> rule5)) -> rule7))]
("Gary" "is" "round" "+")
((((((triple7) -> (rule2 % int3)) triple5) -> (rule5 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not round.
False
5
inv-proof
[(((((((triple7) -> rule2) triple5) -> rule5)) -> rule7))]
("Gary" "is" "round" "-")
((((((triple7) -> (rule2 % int3)) triple5) -> (rule5 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Erin is green.[(triple1)] Erin is round.[(triple2)] Erin is smart.[(triple3)] Gary is green.[(triple4 OR ((triple7 triple5) -> rule8))] Gary is kind.[(triple5)] Gary is not nice.[(triple6 OR ((triple7) -> rule4) OR ((triple5 ((((triple7) -> rule2) triple5) -> rule5)) -> rule6))] Gary is quiet.[(triple7)] @1: Gary is smart.[(((triple7) -> rule2))] @2: Gary is rough.[(((((triple7) -> rule2) triple5) -> rule5))] @3: Gary is round.[(((((((triple7) -> rule2) triple5) -> rule5)) -> rule7))]
Erin is green.
("Erin" "is" "green" "+")
triple1
Erin is round.
("Erin" "is" "round" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple4
((triple7 triple5) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple5
Gary is not nice.
("Gary" "is" "nice" "-")
triple6
((triple7) -> (rule4 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
((triple5 ((((triple7) -> (rule2 % int3)) triple5) -> (rule5 % int2))) -> (rule6 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
Gary is smart.
("Gary" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((((triple7) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((((triple7) -> (rule2 % int3)) triple5) -> (rule5 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3