Charlie is quiet. Charlie is white. Dave is smart. Dave is white. Erin is green. Erin is quiet. Erin is white. If something is rough and smart then it is white. If something is rough then it is white. Round, white things are quiet. All rough, cold things are smart. All white, smart things are cold. Smart, quiet things are round. If something is white then it is round. Cold, green things are smart.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
If something is rough and smart then it is white.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is rough then it is white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Round, white things are quiet.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
All rough, cold things are smart.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
All white, smart things are cold.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Smart, quiet things are round.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If something is white then it is round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Cold, green things are smart.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Erin is green.
True
1
proof
[(triple5)]
("Erin" "is" "green" "+")
triple5
Dave is not white.
False
1
inv-proof
[(triple4)]
("Dave" "is" "white" "-")
triple4
Erin is not cold.
Unknown
inv-rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Erin" "is" "cold" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is quiet.[(triple1 OR ((((triple2) -> rule7) triple2) -> rule3))] Charlie is white.[(triple2)] Dave is smart.[(triple3)] Dave is white.[(triple4)] Erin is green.[(triple5)] Erin is quiet.[(triple6 OR ((((triple7) -> rule7) triple7) -> rule3))] Erin is white.[(triple7)] @1: Charlie is round.[(((triple2) -> rule7))] Dave is cold.[(((triple4 triple3) -> rule5))] Dave is round.[(((triple4) -> rule7))] Erin is round.[(((triple7) -> rule7))] @2: Dave is quiet.[(((((triple4) -> rule7) triple4) -> rule3))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
((((triple2) -> (rule7 % int2)) triple2) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
((((triple7) -> (rule7 % int2)) triple7) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
((triple2) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple4 triple3) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple4) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple7) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple4) -> (rule7 % int2)) triple4) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2