Charlie is blue. Charlie is kind. Charlie is quiet. Charlie is rough. Charlie is smart. Erin is rough. Gary is smart. Rough people are smart. All blue people are quiet. All cold, kind people are blue. All white, blue people are smart. If someone is quiet then they are white. If someone is quiet then they are rough. If someone is cold and kind then they are quiet. If someone is cold and rough then they are quiet.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
All blue people are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
All cold, kind people are blue.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
All white, blue people are smart.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is quiet then they are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold and kind then they are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is cold and rough then they are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Erin is rough.
True
1
proof
[(triple6)]
("Erin" "is" "rough" "+")
triple6
Charlie is not quiet.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule2))]
("Charlie" "is" "quiet" "-")
triple3
((triple1) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
True
2
proof
[(((triple3) -> rule5) OR ((((triple1) -> rule2)) -> rule5))]
("Charlie" "is" "white" "+")
((triple3) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Erin is not smart.
False
2
inv-proof
[(((triple6) -> rule1))]
("Erin" "is" "smart" "-")
((triple6) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is not quiet.
Unknown
inv-rconc
[@2: Gary is quiet.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is white.
Unknown
rconc
[@3: Gary is white.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule3 <- FAIL)]]
("Gary" "is" "white" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Charlie is blue.[(triple1)] Charlie is kind.[(triple2)] Charlie is quiet.[(triple3 OR ((triple1) -> rule2))] Charlie is rough.[(triple4 OR ((triple3) -> rule6) OR ((((triple1) -> rule2)) -> rule6))] Charlie is smart.[(triple5 OR ((triple4) -> rule1) OR ((((triple3) -> rule6)) -> rule1) OR ((((triple3) -> rule5) triple1) -> rule4) OR ((((((triple1) -> rule2)) -> rule6)) -> rule1) OR ((((((triple1) -> rule2)) -> rule5) triple1) -> rule4))] Erin is rough.[(triple6)] Gary is smart.[(triple7)] @1: Charlie is white.[(((triple3) -> rule5) OR ((((triple1) -> rule2)) -> rule5))] Erin is smart.[(((triple6) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
((triple1) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
((triple3) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
((triple4) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple3) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
((triple3) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((triple6) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1