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