Bob is white. Charlie is cold. Fiona is white. Round things are white. All cold things are white. If something is round and not rough then it is quiet. If something is kind and young then it is not quiet. White, cold things are round. If something is round and white then it is not young.
Bob is white.
("Bob" "is" "white" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
All cold things are white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is round and not rough then it is quiet.
((("something" "is" "round" "+") ("something" "is" "rough" "~")) -> ("something" "is" "quiet" "+"))
If something is kind and young then it is not quiet.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "-"))
White, cold things are round.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is round and white then it is not young.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "-"))
Fiona is white.
True
1
proof
[(triple3)]
("Fiona" "is" "white" "+")
triple3
Fiona is not white.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "white" "-")
triple3
Charlie is white.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "white" "+")
((triple2) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple2) -> rule2))]
("Charlie" "is" "white" "-")
((triple2) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
True
4
proof
[(((((triple2) -> rule2) triple2) -> rule5))]
("Charlie" "is" "round" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not round.
False
4
inv-proof
[(((((triple2) -> rule2) triple2) -> rule5))]
("Charlie" "is" "round" "-")
((((triple2) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not young.
True
7
proof
[(((((((triple2) -> rule2) triple2) -> rule5) ((triple2) -> rule2)) -> rule6))]
("Charlie" "is" "young" "-")
((((((triple2) -> (rule2 % int3)) triple2) -> (rule5 % int2)) ((triple2) -> (rule2 % int3))) -> (rule6 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is young.
False
7
inv-proof
[(((((((triple2) -> rule2) triple2) -> rule5) ((triple2) -> rule2)) -> rule6))]
("Charlie" "is" "young" "+")
((((((triple2) -> (rule2 % int3)) triple2) -> (rule5 % int2)) ((triple2) -> (rule2 % int3))) -> (rule6 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "quiet" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Bob is white.[(triple1)] Charlie is cold.[(triple2)] Fiona is white.[(triple3)] @1: Charlie is white.[(((triple2) -> rule2))] @2: Charlie is round.[(((((triple2) -> rule2) triple2) -> rule5))] @3: Charlie is not young.[(((((((triple2) -> rule2) triple2) -> rule5) ((triple2) -> rule2)) -> rule6))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not young.
("Charlie" "is" "young" "-")
((((((triple2) -> (rule2 % int3)) triple2) -> (rule5 % int2)) ((triple2) -> (rule2 % int3))) -> (rule6 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3