Anne is kind. Bob is smart. Fiona is quiet. Gary is kind. If something is quiet then it is green. Quiet, kind things are smart. If something is nice then it is kind. If something is green then it is cold. Blue, green things are cold. All kind things are quiet.
Anne is kind.
("Anne" "is" "kind" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Quiet, kind things are smart.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If something is nice then it is kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Blue, green things are cold.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
All kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Fiona is not quiet.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "quiet" "-")
triple3
Gary is quiet.
True
2
proof
[(((triple4) -> rule6))]
("Gary" "is" "quiet" "+")
((triple4) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Fiona is cold.
True
3
proof
[(((((triple3) -> rule1)) -> rule4))]
("Fiona" "is" "cold" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Anne is not smart.
False
4
inv-proof
[(((((triple1) -> rule6) triple1) -> rule2))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule6 % int2)) triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
True
4
proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule4))]
("Anne" "is" "cold" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Gary is not cold.
False
4
inv-proof
[(((((((triple4) -> rule6)) -> rule1)) -> rule4))]
("Gary" "is" "cold" "-")
((((((triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Bob is not green.
Unknown
inv-rconc
[@3: Bob is green.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule3 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "kind" "+")
Bob is not cold.
Unknown
inv-rconc
[@4: Bob is cold.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule6 <- rule3 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is quiet.
Unknown
rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Bob" "is" "quiet" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is kind.[(triple1)] Bob is smart.[(triple2)] Fiona is quiet.[(triple3)] Gary is kind.[(triple4)] @1: Anne is quiet.[(((triple1) -> rule6))] Fiona is green.[(((triple3) -> rule1))] Gary is quiet.[(((triple4) -> rule6))] @2: Anne is green.[(((((triple1) -> rule6)) -> rule1))] Anne is smart.[(((((triple1) -> rule6) triple1) -> rule2))] Fiona is cold.[(((((triple3) -> rule1)) -> rule4))] Gary is green.[(((((triple4) -> rule6)) -> rule1))] Gary is smart.[(((((triple4) -> rule6) triple4) -> rule2))] @3: Anne is cold.[(((((((triple1) -> rule6)) -> rule1)) -> rule4))] Gary is cold.[(((((((triple4) -> rule6)) -> rule1)) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple3) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple4) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple4) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3