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