Anne is quiet. Bob is blue. Bob is quiet. Bob is white. Fiona is blue. Fiona is white. Gary is blue. Gary is cold. Gary is quiet. Gary is white. If Bob is cold and Bob is red then Bob is kind. All quiet, smart things are blue. All kind things are smart. White things are cold. White, quiet things are red. Cold things are blue.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is white.
("Bob" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
If Bob is cold and Bob is red then Bob is kind.
((("Bob" "is" "cold" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "kind" "+"))
All quiet, smart things are blue.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
All kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
White things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
White, quiet things are red.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Gary is blue.
True
1
proof
[(triple7 OR ((triple8) -> rule6) OR ((((triple10) -> rule4)) -> rule6))]
("Gary" "is" "blue" "+")
triple7
((triple8) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not cold.
False
1
inv-proof
[(triple8 OR ((triple10) -> rule4))]
("Gary" "is" "cold" "-")
triple8
((triple10) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Bob is red.
True
3
proof
[(((triple4 triple3) -> rule5))]
("Bob" "is" "red" "+")
((triple4 triple3) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Fiona is not cold.
False
2
inv-proof
[(((triple6) -> rule4))]
("Fiona" "is" "cold" "-")
((triple6) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Bob is kind.
True
6
proof
[(((((triple4) -> rule4) ((triple4 triple3) -> rule5)) -> rule1))]
("Bob" "is" "kind" "+")
((((triple4) -> (rule4 % int3)) ((triple4 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not kind.
False
6
inv-proof
[(((((triple4) -> rule4) ((triple4 triple3) -> rule5)) -> rule1))]
("Bob" "is" "kind" "-")
((((triple4) -> (rule4 % int3)) ((triple4 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is smart.
True
7
proof
[(((((((triple4) -> rule4) ((triple4 triple3) -> rule5)) -> rule1)) -> rule3))]
("Bob" "is" "smart" "+")
((((((triple4) -> (rule4 % int4)) ((triple4 triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Bob is not smart.
False
7
inv-proof
[(((((((triple4) -> rule4) ((triple4 triple3) -> rule5)) -> rule1)) -> rule3))]
("Bob" "is" "smart" "-")
((((((triple4) -> (rule4 % int4)) ((triple4 triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is cold.
Unknown
rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "cold" "+")
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "red" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "red" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is quiet.[(triple1)] Bob is blue.[(triple2 OR ((((triple4) -> rule4)) -> rule6) OR ((triple3 ((((((triple4) -> rule4) ((triple4 triple3) -> rule5)) -> rule1)) -> rule3)) -> rule2))] Bob is quiet.[(triple3)] Bob is white.[(triple4)] Fiona is blue.[(triple5 OR ((((triple6) -> rule4)) -> rule6))] Fiona is white.[(triple6)] Gary is blue.[(triple7 OR ((triple8) -> rule6) OR ((((triple10) -> rule4)) -> rule6))] Gary is cold.[(triple8 OR ((triple10) -> rule4))] Gary is quiet.[(triple9)] Gary is white.[(triple10)] @1: Bob is cold.[(((triple4) -> rule4))] Bob is red.[(((triple4 triple3) -> rule5))] Fiona is cold.[(((triple6) -> rule4))] Gary is red.[(((triple10 triple9) -> rule5))] @2: Bob is kind.[(((((triple4) -> rule4) ((triple4 triple3) -> rule5)) -> rule1))] @3: Bob is smart.[(((((((triple4) -> rule4) ((triple4 triple3) -> rule5)) -> rule1)) -> rule3))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((triple3 ((((((triple4) -> (rule4 % int5)) ((triple4 triple3) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is cold.
("Bob" "is" "cold" "+")
int5
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
((((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
((triple8) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple8
((triple10) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Bob is cold.
("Bob" "is" "cold" "+")
((triple4) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple4 triple3) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple6) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple10 triple9) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple4) -> (rule4 % int3)) ((triple4 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple4) -> (rule4 % int4)) ((triple4 triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4