Charlie is not kind. Charlie is not quiet. Charlie is not round. Charlie is not white. Dave is kind. Dave is red. Dave is not round. Fiona is cold. Fiona is not round. Fiona is white. If someone is smart then they are round. All white people are cold. Quiet people are white. If someone is cold then they are white. If Charlie is kind then Charlie is quiet. If someone is kind then they are quiet.
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is not round.
("Charlie" "is" "round" "-")
Charlie is not white.
("Charlie" "is" "white" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not round.
("Dave" "is" "round" "-")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Fiona is white.
("Fiona" "is" "white" "+")
If someone is smart then they are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
All white people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
Quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is cold then they are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If Charlie is kind then Charlie is quiet.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "quiet" "+"))
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Dave is kind.
True
1
proof
[(triple5)]
("Dave" "is" "kind" "+")
triple5
Dave is not kind.
False
1
inv-proof
[(triple5)]
("Dave" "is" "kind" "-")
triple5
Dave is quiet.
True
2
proof
[(((triple5) -> rule6))]
("Dave" "is" "quiet" "+")
((triple5) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple5) -> rule6))]
("Dave" "is" "quiet" "-")
((triple5) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
True
3
proof
[(((((triple5) -> rule6)) -> rule3))]
("Dave" "is" "white" "+")
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not white.
False
3
inv-proof
[(((((triple5) -> rule6)) -> rule3))]
("Dave" "is" "white" "-")
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is cold.
True
4
proof
[(((((((triple5) -> rule6)) -> rule3)) -> rule2))]
("Dave" "is" "cold" "+")
((((((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not cold.
False
4
inv-proof
[(((((((triple5) -> rule6)) -> rule3)) -> rule2))]
("Dave" "is" "cold" "-")
((((((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "cold" "-")
Fiona is quiet.
Unknown
rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is not kind.[(triple1)] Charlie is not quiet.[(triple2)] Charlie is not round.[(triple3)] Charlie is not white.[(triple4)] Dave is kind.[(triple5)] Dave is not round.[(triple7)] Dave is red.[(triple6)] Fiona is cold.[(triple8 OR ((triple10) -> rule2))] Fiona is not round.[(triple9)] Fiona is white.[(triple10 OR ((triple8) -> rule4))] @1: Dave is quiet.[(((triple5) -> rule6))] @2: Dave is white.[(((((triple5) -> rule6)) -> rule3))] @3: Dave is cold.[(((((((triple5) -> rule6)) -> rule3)) -> rule2))]
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple2
Charlie is not round.
("Charlie" "is" "round" "-")
triple3
Charlie is not white.
("Charlie" "is" "white" "-")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is not round.
("Dave" "is" "round" "-")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
((triple10) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is not round.
("Fiona" "is" "round" "-")
triple9
Fiona is white.
("Fiona" "is" "white" "+")
triple10
((triple8) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple5) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3