Anne is red. Anne is not round. Bob is not cold. Bob is green. Fiona is big. Fiona is green. Fiona is round. Gary is blue. Gary is not cold. Gary is round. All round things are quiet. Blue things are quiet. All cold things are quiet. If Fiona is blue then Fiona is big. Red, round things are cold. Red things are cold. If something is blue and not round then it is cold. If Gary is not blue and Gary is not big then Gary is not green.
Anne is red.
("Anne" "is" "red" "+")
Anne is not round.
("Anne" "is" "round" "-")
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is green.
("Bob" "is" "green" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is round.
("Gary" "is" "round" "+")
All round things are quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
All cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If Fiona is blue then Fiona is big.
((("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "big" "+"))
Red, round things are cold.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is blue and not round then it is cold.
((("something" "is" "blue" "+") ("something" "is" "round" "~")) -> ("something" "is" "cold" "+"))
If Gary is not blue and Gary is not big then Gary is not green.
((("Gary" "is" "blue" "~") ("Gary" "is" "big" "~")) -> ("Gary" "is" "green" "-"))
Fiona is round.
True
1
proof
[(triple7)]
("Fiona" "is" "round" "+")
triple7
Bob is not green.
False
1
inv-proof
[(triple4)]
("Bob" "is" "green" "-")
triple4
Anne is cold.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "cold" "-")
((triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
True
3
proof
[(((((triple1) -> rule6)) -> rule3))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not quiet.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule3))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "cold" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "quiet" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is not round.[(triple2)] Anne is red.[(triple1)] Bob is green.[(triple4)] Bob is not cold.[(triple3)] Fiona is big.[(triple5)] Fiona is green.[(triple6)] Fiona is round.[(triple7)] Gary is blue.[(triple8)] Gary is not cold.[(triple9)] Gary is round.[(triple10)] @1: Anne is cold.[(((triple1) -> rule6))] Fiona is quiet.[(((triple7) -> rule1))] Gary is quiet.[(((triple10) -> rule1) OR ((triple8) -> rule2))] @2: Anne is quiet.[(((((triple1) -> rule6)) -> rule3))]
Anne is not round.
("Anne" "is" "round" "-")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is not cold.
("Bob" "is" "cold" "-")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Fiona is round.
("Fiona" "is" "round" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Gary is not cold.
("Gary" "is" "cold" "-")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple10
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple7) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple10) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple8) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2