Charlie is green. Fiona is blue. Gary is quiet. Quiet things are cold. All cold things are green. All big things are nice. All green things are white. White things are blue. If Gary is blue and Gary is cold then Gary is nice.
Charlie is green.
("Charlie" "is" "green" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
All cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
All green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
White things are blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If Gary is blue and Gary is cold then Gary is nice.
((("Gary" "is" "blue" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "nice" "+"))
Gary is quiet.
True
1
proof
[(triple3)]
("Gary" "is" "quiet" "+")
triple3
Charlie is not green.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "green" "-")
triple1
Charlie is white.
True
2
proof
[(((triple1) -> rule4))]
("Charlie" "is" "white" "+")
((triple1) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple1) -> rule4))]
("Charlie" "is" "white" "-")
((triple1) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is green.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("Gary" "is" "green" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Charlie is not blue.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("Charlie" "is" "blue" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Gary is white.
True
4
proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule4))]
("Gary" "is" "white" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not white.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule4))]
("Gary" "is" "white" "-")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "cold" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Fiona is green.
Unknown
rconc
[@2: Fiona is green.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "green" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is green.[(triple1)] Fiona is blue.[(triple2)] Gary is quiet.[(triple3)] @1: Charlie is white.[(((triple1) -> rule4))] Gary is cold.[(((triple3) -> rule1))] @2: Charlie is blue.[(((((triple1) -> rule4)) -> rule5))] Gary is green.[(((((triple3) -> rule1)) -> rule2))] @3: Gary is white.[(((((((triple3) -> rule1)) -> rule2)) -> rule4))] @4: Gary is blue.[(((((((((triple3) -> rule1)) -> rule2)) -> rule4)) -> rule5))] @5: Gary is nice.[(((((((((((triple3) -> rule1)) -> rule2)) -> rule4)) -> rule5) ((triple3) -> rule1)) -> rule6))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((((((((triple3) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is nice.
("Gary" "is" "nice" "+")
((((((((((triple3) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) ((triple3) -> (rule1 % int5))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
int5