Charlie is young. Fiona is nice. Harry is round. All white things are round. Nice things are white. Round, quiet things are not nice. White, round things are not blue. If Charlie is not cold then Charlie is not young. If Charlie is quiet then Charlie is round.
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
All white things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Round, quiet things are not nice.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "-"))
White, round things are not blue.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "-"))
If Charlie is not cold then Charlie is not young.
((("Charlie" "is" "cold" "~")) -> ("Charlie" "is" "young" "-"))
If Charlie is quiet then Charlie is round.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "round" "+"))
Fiona is nice.
True
1
proof
[(triple2)]
("Fiona" "is" "nice" "+")
triple2
Charlie is not young.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "young" "-")
triple1
Fiona is white.
True
2
proof
[(((triple2) -> rule2))]
("Fiona" "is" "white" "+")
((triple2) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is not white.
False
2
inv-proof
[(((triple2) -> rule2))]
("Fiona" "is" "white" "-")
((triple2) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is round.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Fiona" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is not round.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Fiona" "is" "round" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is not blue.
True
6
proof
[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule4))]
("Fiona" "is" "blue" "-")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is blue.
False
6
inv-proof
[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule4))]
("Fiona" "is" "blue" "+")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "white" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is young.[(triple1)] Fiona is nice.[(triple2)] Harry is round.[(triple3)] @1: Fiona is white.[(((triple2) -> rule2))] @2: Fiona is round.[(((((triple2) -> rule2)) -> rule1))] @3: Fiona is not blue.[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule4))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Fiona is white.
("Fiona" "is" "white" "+")
((triple2) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is not blue.
("Fiona" "is" "blue" "-")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3