Bob is kind. Erin is white. Fiona is not quiet. Gary is cold. If something is big and cold then it is red. If something is nice then it is quiet. Kind things are quiet. All white, kind things are big. All nice things are white. Quiet things are nice. If something is white and not cold then it is not nice. If something is big then it is nice.
Bob is kind.
("Bob" "is" "kind" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
Gary is cold.
("Gary" "is" "cold" "+")
If something is big and cold then it is red.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is nice then it is quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
Kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
All white, kind things are big.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
All nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Quiet things are nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
If something is white and not cold then it is not nice.
((("something" "is" "white" "+") ("something" "is" "cold" "~")) -> ("something" "is" "nice" "-"))
If something is big then it is nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Erin is white.
True
1
proof
[(triple2)]
("Erin" "is" "white" "+")
triple2
Erin is not white.
False
1
inv-proof
[(triple2)]
("Erin" "is" "white" "-")
triple2
Bob is quiet.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
True
4
proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule5))]
("Bob" "is" "white" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not white.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule5))]
("Bob" "is" "white" "-")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "red" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "big" "+")
Gary is not white.
Unknown
inv-rconc
[@5: Gary is white.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule2 <- rule8 <- rule4 <- FAIL)]]
("Gary" "is" "white" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "red" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Bob is kind.[(triple1)] Erin is white.[(triple2)] Fiona is not quiet.[(triple3)] Gary is cold.[(triple4)] @1: Bob is quiet.[(((triple1) -> rule3))] @2: Bob is nice.[(((((triple1) -> rule3)) -> rule6))] @3: Bob is white.[(((((((triple1) -> rule3)) -> rule6)) -> rule5))] @4: Bob is big.[(((((((((triple1) -> rule3)) -> rule6)) -> rule5) triple1) -> rule4))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4