Bob is smart. Erin is quiet. Fiona is green. All young, round people are kind. If Bob is round then Bob is kind. If Bob is nice then Bob is green. If someone is green then they are young. If someone is nice and young then they are quiet. If someone is young then they are nice.
Bob is smart.
("Bob" "is" "smart" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is green.
("Fiona" "is" "green" "+")
All young, round people are kind.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If Bob is round then Bob is kind.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "kind" "+"))
If Bob is nice then Bob is green.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "green" "+"))
If someone is green then they are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is nice and young then they are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If someone is young then they are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Erin is quiet.
True
1
proof
[(triple2)]
("Erin" "is" "quiet" "+")
triple2
Bob is not smart.
False
1
inv-proof
[(triple1)]
("Bob" "is" "smart" "-")
triple1
Fiona is young.
True
2
proof
[(((triple3) -> rule4))]
("Fiona" "is" "young" "+")
((triple3) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is not young.
False
2
inv-proof
[(((triple3) -> rule4))]
("Fiona" "is" "young" "-")
((triple3) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is nice.
True
3
proof
[(((((triple3) -> rule4)) -> rule6))]
("Fiona" "is" "nice" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not nice.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule6))]
("Fiona" "is" "nice" "-")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is quiet.
True
6
proof
[(((((((triple3) -> rule4)) -> rule6) ((triple3) -> rule4)) -> rule5))]
("Fiona" "is" "quiet" "+")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2)) ((triple3) -> (rule4 % int3))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is not quiet.
False
6
inv-proof
[(((((((triple3) -> rule4)) -> rule6) ((triple3) -> rule4)) -> rule5))]
("Fiona" "is" "quiet" "-")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2)) ((triple3) -> (rule4 % int3))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@4: Bob is quiet.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule4 <- rule3 <- FAIL)]]
("Bob" "is" "quiet" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "young" "+")
Bob is not nice.
Unknown
inv-rconc
[@3: Bob is nice.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule3 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is green.
Unknown
rconc
[@3: Bob is green.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule4 <- FAIL)]]
("Bob" "is" "green" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Bob is smart.[(triple1)] Erin is quiet.[(triple2)] Fiona is green.[(triple3)] @1: Fiona is young.[(((triple3) -> rule4))] @2: Fiona is nice.[(((((triple3) -> rule4)) -> rule6))] @3: Fiona is quiet.[(((((((triple3) -> rule4)) -> rule6) ((triple3) -> rule4)) -> rule5))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Fiona is young.
("Fiona" "is" "young" "+")
((triple3) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2)) ((triple3) -> (rule4 % int3))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3