Charlie is quiet. Charlie is red. Charlie is rough. Charlie is white. Dave is blue. Dave is quiet. Dave is red. Dave is rough. Erin is kind. Erin is quiet. Erin is red. Erin is rough. Erin is smart. Gary is blue. Gary is kind. Gary is rough. If something is quiet and white then it is red. All white things are kind. All rough, kind things are red. White things are quiet. If something is red then it is quiet. If something is smart then it is blue.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If something is quiet and white then it is red.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All white things are kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
All rough, kind things are red.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
White things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is red then it is quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If something is smart then it is blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Dave is quiet.
True
1
proof
[(triple6 OR ((triple7) -> rule5))]
("Dave" "is" "quiet" "+")
triple6
((triple7) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Charlie is not rough.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "rough" "-")
triple3
Gary is red.
True
3
proof
[(((triple16 triple15) -> rule3))]
("Gary" "is" "red" "+")
((triple16 triple15) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple13) -> rule6))]
("Erin" "is" "blue" "-")
((triple13) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "blue" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "kind" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Charlie is quiet.[(triple1 OR ((triple2) -> rule5) OR ((triple4) -> rule4) OR ((((triple3 ((triple4) -> rule2)) -> rule3)) -> rule5))] Charlie is red.[(triple2 OR ((triple1 triple4) -> rule1) OR ((triple3 ((triple4) -> rule2)) -> rule3) OR ((((triple4) -> rule4) triple4) -> rule1))] Charlie is rough.[(triple3)] Charlie is white.[(triple4)] Dave is blue.[(triple5)] Dave is quiet.[(triple6 OR ((triple7) -> rule5))] Dave is red.[(triple7)] Dave is rough.[(triple8)] Erin is kind.[(triple9)] Erin is quiet.[(triple10 OR ((triple11) -> rule5) OR ((((triple12 triple9) -> rule3)) -> rule5))] Erin is red.[(triple11 OR ((triple12 triple9) -> rule3))] Erin is rough.[(triple12)] Erin is smart.[(triple13)] Gary is blue.[(triple14)] Gary is kind.[(triple15)] Gary is rough.[(triple16)] @1: Charlie is kind.[(((triple4) -> rule2))] Erin is blue.[(((triple13) -> rule6))] Gary is red.[(((triple16 triple15) -> rule3))] @2: Gary is quiet.[(((((triple16 triple15) -> rule3)) -> rule5))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
((triple2) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple4) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple3 ((triple4) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
triple2
((triple1 triple4) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple3 ((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple4) -> (rule4 % int2)) triple4) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
((triple7) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple7
Dave is rough.
("Dave" "is" "rough" "+")
triple8
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
((triple11) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple12 triple9) -> (rule3 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple11
((triple12 triple9) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple12
Erin is smart.
("Erin" "is" "smart" "+")
triple13
Gary is blue.
("Gary" "is" "blue" "+")
triple14
Gary is kind.
("Gary" "is" "kind" "+")
triple15
Gary is rough.
("Gary" "is" "rough" "+")
triple16
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple4) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple13) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple16 triple15) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple16 triple15) -> (rule3 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2