Charlie is smart. Fiona is smart. If Charlie is nice then Charlie is smart. If something is quiet then it is red. If Charlie is smart then Charlie is quiet. If something is round then it is not smart. If something is red then it is young. Nice things are not young.
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If Charlie is nice then Charlie is smart.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "smart" "+"))
If something is quiet then it is red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If Charlie is smart then Charlie is quiet.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "quiet" "+"))
If something is round then it is not smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "-"))
If something is red then it is young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Nice things are not young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "-"))
Fiona is smart.
True
1
proof
[(triple2)]
("Fiona" "is" "smart" "+")
triple2
Charlie is not smart.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "smart" "-")
triple1
Charlie is quiet.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not red.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "red" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
True
4
proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule5))]
("Charlie" "is" "young" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is not young.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule5))]
("Charlie" "is" "young" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Fiona is not young.
Unknown
inv-rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Fiona" "is" "young" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Charlie is smart.[(triple1)] Fiona is smart.[(triple2)] @1: Charlie is quiet.[(((triple1) -> rule3))] @2: Charlie is red.[(((((triple1) -> rule3)) -> rule2))] @3: Charlie is young.[(((((((triple1) -> rule3)) -> rule2)) -> rule5))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3