Charlie is green. Charlie is round. Dave is blue. Dave is cold. Dave is green. Dave is quiet. Erin is cold. Erin is green. Erin is quiet. Erin is rough. Erin is round. Gary is blue. Gary is cold. Gary is green. Gary is round. All green people are rough. Rough, young people are blue. If someone is rough and blue then they are quiet.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is round.
("Gary" "is" "round" "+")
All green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Rough, young people are blue.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough and blue then they are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
Erin is round.
True
1
proof
[(triple11)]
("Erin" "is" "round" "+")
triple11
Erin is not round.
False
1
inv-proof
[(triple11)]
("Erin" "is" "round" "-")
triple11
Dave is rough.
True
2
proof
[(((triple5) -> rule1))]
("Dave" "is" "rough" "+")
((triple5) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "rough" "-")
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Gary is quiet.
True
4
proof
[(((((triple14) -> rule1) triple12) -> rule3))]
("Gary" "is" "quiet" "+")
((((triple14) -> (rule1 % int2)) triple12) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not quiet.
False
4
inv-proof
[(((((triple14) -> rule1) triple12) -> rule3))]
("Gary" "is" "quiet" "-")
((((triple14) -> (rule1 % int2)) triple12) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Charlie is not quiet.
Unknown
inv-rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "blue" "+")
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "blue" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Charlie is green.[(triple1)] Charlie is round.[(triple2)] Dave is blue.[(triple3)] Dave is cold.[(triple4)] Dave is green.[(triple5)] Dave is quiet.[(triple6 OR ((((triple5) -> rule1) triple3) -> rule3))] Erin is cold.[(triple7)] Erin is green.[(triple8)] Erin is quiet.[(triple9)] Erin is rough.[(triple10 OR ((triple8) -> rule1))] Erin is round.[(triple11)] Gary is blue.[(triple12)] Gary is cold.[(triple13)] Gary is green.[(triple14)] Gary is round.[(triple15)] @1: Charlie is rough.[(((triple1) -> rule1))] Dave is rough.[(((triple5) -> rule1))] Gary is rough.[(((triple14) -> rule1))] @2: Gary is quiet.[(((((triple14) -> rule1) triple12) -> rule3))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
((((triple5) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple7
Erin is green.
("Erin" "is" "green" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
Erin is rough.
("Erin" "is" "rough" "+")
triple10
((triple8) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple11
Gary is blue.
("Gary" "is" "blue" "+")
triple12
Gary is cold.
("Gary" "is" "cold" "+")
triple13
Gary is green.
("Gary" "is" "green" "+")
triple14
Gary is round.
("Gary" "is" "round" "+")
triple15
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple5) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple14) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple14) -> (rule1 % int2)) triple12) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2