Bob is nice. Charlie is big. Erin is quiet. Fiona is white. If someone is furry then they are white. If someone is young then they are white. If Erin is young and Erin is nice then Erin is furry. Quiet people are young. White people are red. If Erin is furry and Erin is quiet then Erin is red.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If someone is furry then they are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If someone is young then they are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If Erin is young and Erin is nice then Erin is furry.
((("Erin" "is" "young" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "furry" "+"))
Quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
White people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If Erin is furry and Erin is quiet then Erin is red.
((("Erin" "is" "furry" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "red" "+"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Fiona is not white.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "white" "-")
triple4
Fiona is red.
True
2
proof
[(((triple4) -> rule5))]
("Fiona" "is" "red" "+")
((triple4) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple4) -> rule5))]
("Fiona" "is" "red" "-")
((triple4) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Erin is white.
True
3
proof
[(((((triple3) -> rule4)) -> rule2))]
("Erin" "is" "white" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not white.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule2))]
("Erin" "is" "white" "-")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
True
4
proof
[(((((((triple3) -> rule4)) -> rule2)) -> rule5))]
("Erin" "is" "red" "+")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not red.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule2)) -> rule5))]
("Erin" "is" "red" "-")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Bob is not red.
Unknown
inv-rconc
[@3: Bob is red.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule4 <- FAIL)]]
("Bob" "is" "red" "-")
Charlie is white.
Unknown
rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Charlie" "is" "white" "+")
Bob is not white.
Unknown
inv-rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Bob" "is" "white" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "young" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Bob is nice.[(triple1)] Charlie is big.[(triple2)] Erin is quiet.[(triple3)] Fiona is white.[(triple4)] @1: Erin is young.[(((triple3) -> rule4))] Fiona is red.[(((triple4) -> rule5))] @2: Erin is white.[(((((triple3) -> rule4)) -> rule2))] @3: Erin is red.[(((((((triple3) -> rule4)) -> rule2)) -> rule5))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Fiona is white.
("Fiona" "is" "white" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
((triple3) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple4) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3