Bob is not green. Bob is round. Charlie is kind. Charlie is round. Fiona is not cold. Fiona is kind. Gary is green. Kind, blue things are not round. If something is quiet and white then it is not round. If Fiona is blue and Fiona is not cold then Fiona is quiet. Blue things are green. If Gary is green then Gary is cold. Green, white things are not kind. If something is quiet and blue then it is white. All cold, green things are quiet. Green, quiet things are blue.
Bob is not green.
("Bob" "is" "green" "-")
Bob is round.
("Bob" "is" "round" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is not cold.
("Fiona" "is" "cold" "-")
Fiona is kind.
("Fiona" "is" "kind" "+")
Gary is green.
("Gary" "is" "green" "+")
Kind, blue things are not round.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "-"))
If something is quiet and white then it is not round.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "round" "-"))
If Fiona is blue and Fiona is not cold then Fiona is quiet.
((("Fiona" "is" "blue" "+") ("Fiona" "is" "cold" "~")) -> ("Fiona" "is" "quiet" "+"))
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If Gary is green then Gary is cold.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "cold" "+"))
Green, white things are not kind.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "-"))
If something is quiet and blue then it is white.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
All cold, green things are quiet.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Green, quiet things are blue.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Charlie is kind.
True
1
proof
[(triple3)]
("Charlie" "is" "kind" "+")
triple3
Charlie is not round.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "round" "-")
triple4
Gary is cold.
True
2
proof
[(((triple7) -> rule5))]
("Gary" "is" "cold" "+")
((triple7) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple7) -> rule5))]
("Gary" "is" "cold" "-")
((triple7) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
True
4
proof
[(((((triple7) -> rule5) triple7) -> rule8))]
("Gary" "is" "quiet" "+")
((((triple7) -> (rule5 % int2)) triple7) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not quiet.
False
4
inv-proof
[(((((triple7) -> rule5) triple7) -> rule8))]
("Gary" "is" "quiet" "-")
((((triple7) -> (rule5 % int2)) triple7) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is blue.
True
6
proof
[(((triple7 ((((triple7) -> rule5) triple7) -> rule8)) -> rule9))]
("Gary" "is" "blue" "+")
((triple7 ((((triple7) -> (rule5 % int3)) triple7) -> (rule8 % int2))) -> (rule9 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not blue.
False
6
inv-proof
[(((triple7 ((((triple7) -> rule5) triple7) -> rule8)) -> rule9))]
("Gary" "is" "blue" "-")
((triple7 ((((triple7) -> (rule5 % int3)) triple7) -> (rule8 % int2))) -> (rule9 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is white.
True
11
proof
[(((((((triple7) -> rule5) triple7) -> rule8) ((triple7 ((((triple7) -> rule5) triple7) -> rule8)) -> rule9)) -> rule7))]
("Gary" "is" "white" "+")
((((((triple7) -> (rule5 % int4)) triple7) -> (rule8 % int3)) ((triple7 ((((triple7) -> (rule5 % int4)) triple7) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is not white.
False
11
inv-proof
[(((((((triple7) -> rule5) triple7) -> rule8) ((triple7 ((((triple7) -> rule5) triple7) -> rule8)) -> rule9)) -> rule7))]
("Gary" "is" "white" "-")
((((((triple7) -> (rule5 % int4)) triple7) -> (rule8 % int3)) ((triple7 ((((triple7) -> (rule5 % int4)) triple7) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is not kind.
True
13
proof
[(((triple7 ((((((triple7) -> rule5) triple7) -> rule8) ((triple7 ((((triple7) -> rule5) triple7) -> rule8)) -> rule9)) -> rule7)) -> rule6))]
("Gary" "is" "kind" "-")
((triple7 ((((((triple7) -> (rule5 % int5)) triple7) -> (rule8 % int4)) ((triple7 ((((triple7) -> (rule5 % int5)) triple7) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
int5
Gary is round.
False
16
inv-proof
[(((((((triple7) -> rule5) triple7) -> rule8) ((((((triple7) -> rule5) triple7) -> rule8) ((triple7 ((((triple7) -> rule5) triple7) -> rule8)) -> rule9)) -> rule7)) -> rule2))]
("Gary" "is" "round" "+")
((((((triple7) -> (rule5 % int5)) triple7) -> (rule8 % int4)) ((((((triple7) -> (rule5 % int5)) triple7) -> (rule8 % int4)) ((triple7 ((((triple7) -> (rule5 % int5)) triple7) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
int5
Charlie is not green.
Unknown
inv-rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule4 <- rule9 <- FAIL)]]
("Charlie" "is" "green" "-")
Fiona is white.
Unknown
rconc
[@2: Fiona is white.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Fiona" "is" "white" "+")
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Bob" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule9 <- rule4 <- FAIL)]]
("Charlie" "is" "blue" "-")
Fiona is quiet.
Unknown
rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is not green.[(triple1)] Bob is round.[(triple2)] Charlie is kind.[(triple3)] Charlie is round.[(triple4)] Fiona is kind.[(triple6)] Fiona is not cold.[(triple5)] Gary is green.[(triple7)] @1: Gary is cold.[(((triple7) -> rule5))] @2: Gary is quiet.[(((((triple7) -> rule5) triple7) -> rule8))] @3: Gary is blue.[(((triple7 ((((triple7) -> rule5) triple7) -> rule8)) -> rule9))] @4: Gary is white.[(((((((triple7) -> rule5) triple7) -> rule8) ((triple7 ((((triple7) -> rule5) triple7) -> rule8)) -> rule9)) -> rule7))] @5: Gary is not kind.[(((triple7 ((((((triple7) -> rule5) triple7) -> rule8) ((triple7 ((((triple7) -> rule5) triple7) -> rule8)) -> rule9)) -> rule7)) -> rule6))] Gary is not round.[(((((((triple7) -> rule5) triple7) -> rule8) ((((((triple7) -> rule5) triple7) -> rule8) ((triple7 ((((triple7) -> rule5) triple7) -> rule8)) -> rule9)) -> rule7)) -> rule2))]
Bob is not green.
("Bob" "is" "green" "-")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Fiona is kind.
("Fiona" "is" "kind" "+")
triple6
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
((triple7) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple7) -> (rule5 % int2)) triple7) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((triple7 ((((triple7) -> (rule5 % int3)) triple7) -> (rule8 % int2))) -> (rule9 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((((((triple7) -> (rule5 % int4)) triple7) -> (rule8 % int3)) ((triple7 ((((triple7) -> (rule5 % int4)) triple7) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is not kind.
("Gary" "is" "kind" "-")
((triple7 ((((((triple7) -> (rule5 % int5)) triple7) -> (rule8 % int4)) ((triple7 ((((triple7) -> (rule5 % int5)) triple7) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
int5
Gary is not round.
("Gary" "is" "round" "-")
((((((triple7) -> (rule5 % int5)) triple7) -> (rule8 % int4)) ((((((triple7) -> (rule5 % int5)) triple7) -> (rule8 % int4)) ((triple7 ((((triple7) -> (rule5 % int5)) triple7) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
int5