Anne is not green. Bob is green. Charlie is round. Fiona is quiet. If someone is round then they are not nice. If someone is green then they are round. If someone is green and not nice then they are quiet.
Anne is not green.
("Anne" "is" "green" "-")
Bob is green.
("Bob" "is" "green" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If someone is round then they are not nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "-"))
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone is green and not nice then they are quiet.
((("someone" "is" "green" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "quiet" "+"))
Fiona is quiet.
True
1
proof
[(triple4)]
("Fiona" "is" "quiet" "+")
triple4
Bob is not green.
False
1
inv-proof
[(triple2)]
("Bob" "is" "green" "-")
triple2
Charlie is not nice.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Bob is not round.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "round" "-")
((triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not nice.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "nice" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is nice.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
True
5
proof
[(((triple2 ((((triple2) -> rule2)) -> rule1)) -> rule3))]
("Bob" "is" "quiet" "+")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not quiet.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule2)) -> rule1)) -> rule3))]
("Bob" "is" "quiet" "-")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "quiet" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "round" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "round" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Anne is not green.[(triple1)] Bob is green.[(triple2)] Charlie is round.[(triple3)] Fiona is quiet.[(triple4)] @1: Bob is round.[(((triple2) -> rule2))] Charlie is not nice.[(((triple3) -> rule1))] @2: Bob is not nice.[(((((triple2) -> rule2)) -> rule1))] @3: Bob is quiet.[(((triple2 ((((triple2) -> rule2)) -> rule1)) -> rule3))]
Anne is not green.
("Anne" "is" "green" "-")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is not nice.
("Charlie" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
int2
Bob is round.
("Bob" "is" "round" "+")
int3