Anne is not big. Bob is cold. Charlie is big. Fiona is cold. All big things are furry. If something is rough and young then it is furry. If something is furry then it is not white. Big, rough things are white. If Fiona is furry then Fiona is big. If something is rough then it is not cold.
Anne is not big.
("Anne" "is" "big" "-")
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
All big things are furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If something is rough and young then it is furry.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If something is furry then it is not white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "-"))
Big, rough things are white.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If Fiona is furry then Fiona is big.
((("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "big" "+"))
If something is rough then it is not cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "-"))
Anne is not big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Charlie is furry.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "furry" "-")
((triple3) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not white.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("Charlie" "is" "white" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("Charlie" "is" "white" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "white" "-")
Fiona is furry.
Unknown
rconc
[@3: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule2 <- FAIL)]]
("Fiona" "is" "furry" "+")
Fiona is not big.
Unknown
inv-rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Fiona" "is" "big" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Anne is not big.[(triple1)] Bob is cold.[(triple2)] Charlie is big.[(triple3)] Fiona is cold.[(triple4)] @1: Charlie is furry.[(((triple3) -> rule1))] @2: Charlie is not white.[(((((triple3) -> rule1)) -> rule3))]
Anne is not big.
("Anne" "is" "big" "-")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not white.
("Charlie" "is" "white" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2