Bob is round. Charlie is cold. Erin is green. Gary is big. If Charlie is not quiet then Charlie is not round. If something is green and red then it is not big. If something is red and nice then it is not green. Cold things are green. All green, big things are cold. Green, cold things are red.
Bob is round.
("Bob" "is" "round" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Gary is big.
("Gary" "is" "big" "+")
If Charlie is not quiet then Charlie is not round.
((("Charlie" "is" "quiet" "~")) -> ("Charlie" "is" "round" "-"))
If something is green and red then it is not big.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "-"))
If something is red and nice then it is not green.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "-"))
Cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
All green, big things are cold.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
Green, cold things are red.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Gary is big.
True
1
proof
[(triple4)]
("Gary" "is" "big" "+")
triple4
Gary is not big.
False
1
inv-proof
[(triple4)]
("Gary" "is" "big" "-")
triple4
Charlie is green.
True
2
proof
[(((triple2) -> rule4))]
("Charlie" "is" "green" "+")
((triple2) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple2) -> rule4))]
("Charlie" "is" "green" "-")
((triple2) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
True
4
proof
[(((((triple2) -> rule4) triple2) -> rule6))]
("Charlie" "is" "red" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not red.
False
4
inv-proof
[(((((triple2) -> rule4) triple2) -> rule6))]
("Charlie" "is" "red" "-")
((((triple2) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not big.
True
7
proof
[(((((triple2) -> rule4) ((((triple2) -> rule4) triple2) -> rule6)) -> rule2))]
("Charlie" "is" "big" "-")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3)) triple2) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is big.
False
7
inv-proof
[(((((triple2) -> rule4) ((((triple2) -> rule4) triple2) -> rule6)) -> rule2))]
("Charlie" "is" "big" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3)) triple2) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Bob is not green.
Unknown
inv-rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Bob" "is" "green" "-")
Erin is red.
Unknown
rconc
[@2: Erin is red.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Erin" "is" "red" "+")
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "cold" "-")
Gary is cold.
Unknown
rconc
[@2: Gary is cold.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Gary" "is" "cold" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is round.[(triple1)] Charlie is cold.[(triple2)] Erin is green.[(triple3)] Gary is big.[(triple4)] @1: Charlie is green.[(((triple2) -> rule4))] @2: Charlie is red.[(((((triple2) -> rule4) triple2) -> rule6))] @3: Charlie is not big.[(((((triple2) -> rule4) ((((triple2) -> rule4) triple2) -> rule6)) -> rule2))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Charlie is green.
("Charlie" "is" "green" "+")
((triple2) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not big.
("Charlie" "is" "big" "-")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3)) triple2) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3