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