Charlie is blue. Charlie is cold. Charlie is white. Dave is blue. Dave is quiet. Gary is blue. Gary is round. Harry is not green. Harry is quiet. Harry is not white. Red, round people are cold. All red people are green. If someone is green then they are round. If Dave is not blue then Dave is not green. If someone is blue then they are red. All cold people are red. All cold people are white. If Gary is green and Gary is cold then Gary is red.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is not green.
("Harry" "is" "green" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not white.
("Harry" "is" "white" "-")
Red, round people are cold.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
All red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If Dave is not blue then Dave is not green.
((("Dave" "is" "blue" "~")) -> ("Dave" "is" "green" "-"))
If someone is blue then they are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
All cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
All cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If Gary is green and Gary is cold then Gary is red.
((("Gary" "is" "green" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "red" "+"))
Harry is not white.
True
1
proof
[(triple10)]
("Harry" "is" "white" "-")
triple10
Charlie is not blue.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "blue" "-")
triple1
Dave is red.
True
2
proof
[(((triple4) -> rule5))]
("Dave" "is" "red" "+")
((triple4) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple2) -> rule6))]
("Charlie" "is" "red" "-")
((triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple2) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
True
3
proof
[(((((triple1) -> rule5)) -> rule2) OR ((((triple2) -> rule6)) -> rule2))]
("Charlie" "is" "green" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule2))]
("Gary" "is" "green" "-")
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is white.
True
5
proof
[(((((((triple6) -> rule5) triple7) -> rule1)) -> rule7) OR ((((((triple6) -> rule5) ((((((triple6) -> rule5)) -> rule2)) -> rule3)) -> rule1)) -> rule7))]
("Gary" "is" "white" "+")
((((((triple6) -> (rule5 % int3)) triple7) -> (rule1 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((triple6) -> (rule5 % int5)) ((((((triple6) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5
Charlie is not round.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule3) OR ((((((triple2) -> rule6)) -> rule2)) -> rule3))]
("Charlie" "is" "round" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Dave is cold.
True
7
proof
[(((((triple4) -> rule5) ((((((triple4) -> rule5)) -> rule2)) -> rule3)) -> rule1))]
("Dave" "is" "cold" "+")
((((triple4) -> (rule5 % int4)) ((((((triple4) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is not cold.
False
7
inv-proof
[(((((triple4) -> rule5) ((((((triple4) -> rule5)) -> rule2)) -> rule3)) -> rule1))]
("Dave" "is" "cold" "-")
((((triple4) -> (rule5 % int4)) ((((((triple4) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is white.
True
8
proof
[(((((((triple4) -> rule5) ((((((triple4) -> rule5)) -> rule2)) -> rule3)) -> rule1)) -> rule7))]
("Dave" "is" "white" "+")
((((((triple4) -> (rule5 % int5)) ((((((triple4) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5
Dave is not white.
False
8
inv-proof
[(((((((triple4) -> rule5) ((((((triple4) -> rule5)) -> rule2)) -> rule3)) -> rule1)) -> rule7))]
("Dave" "is" "white" "-")
((((((triple4) -> (rule5 % int5)) ((((((triple4) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5
Harry is not red.
Unknown
inv-rconc
[@3: Harry is red.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule5 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "round" "+")
Harry is not cold.
Unknown
inv-rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Harry" "is" "cold" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2 OR ((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule2)) -> rule3)) -> rule1))] Charlie is white.[(triple3 OR ((triple2) -> rule7) OR ((((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule2)) -> rule3)) -> rule1)) -> rule7))] Dave is blue.[(triple4)] Dave is quiet.[(triple5)] Gary is blue.[(triple6)] Gary is round.[(triple7 OR ((((((triple6) -> rule5)) -> rule2)) -> rule3))] Harry is not green.[(triple8)] Harry is not white.[(triple10)] Harry is quiet.[(triple9)] @1: Charlie is red.[(((triple1) -> rule5) OR ((triple2) -> rule6))] Dave is red.[(((triple4) -> rule5))] Gary is red.[(((triple6) -> rule5))] @2: Charlie is green.[(((((triple1) -> rule5)) -> rule2) OR ((((triple2) -> rule6)) -> rule2))] Dave is green.[(((((triple4) -> rule5)) -> rule2))] Gary is cold.[(((((triple6) -> rule5) triple7) -> rule1) OR ((((triple6) -> rule5) ((((((triple6) -> rule5)) -> rule2)) -> rule3)) -> rule1))] Gary is green.[(((((triple6) -> rule5)) -> rule2))] @3: Charlie is round.[(((((((triple1) -> rule5)) -> rule2)) -> rule3) OR ((((((triple2) -> rule6)) -> rule2)) -> rule3))] Dave is round.[(((((((triple4) -> rule5)) -> rule2)) -> rule3))] Gary is white.[(((((((triple6) -> rule5) triple7) -> rule1)) -> rule7) OR ((((((triple6) -> rule5) ((((((triple6) -> rule5)) -> rule2)) -> rule3)) -> rule1)) -> rule7))] @4: Dave is cold.[(((((triple4) -> rule5) ((((((triple4) -> rule5)) -> rule2)) -> rule3)) -> rule1))] @5: Dave is white.[(((((((triple4) -> rule5) ((((((triple4) -> rule5)) -> rule2)) -> rule3)) -> rule1)) -> rule7))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((((triple1) -> (rule5 % int4)) ((((((triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
triple3
((triple2) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((((triple1) -> (rule5 % int5)) ((((((triple1) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
int5
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
((((((triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Harry is not green.
("Harry" "is" "green" "-")
triple8
Harry is not white.
("Harry" "is" "white" "-")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple2) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple4) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple6) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple6) -> (rule5 % int2)) triple7) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple6) -> (rule5 % int4)) ((((((triple6) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is green.
("Gary" "is" "green" "+")
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((((((triple6) -> (rule5 % int3)) triple7) -> (rule1 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((triple6) -> (rule5 % int5)) ((((((triple6) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5
Dave is cold.
("Dave" "is" "cold" "+")
((((triple4) -> (rule5 % int4)) ((((((triple4) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
((((((triple4) -> (rule5 % int5)) ((((((triple4) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5