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