Bob is big. Bob is kind. Bob is white. Dave is blue. Dave is furry. Dave is white. Fiona is cold. If someone is cold and furry then they are young. Furry people are cold. If someone is young then they are kind.
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
If someone is cold and furry then they are young.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If someone is young then they are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Dave is not blue.
False
1
inv-proof
[(triple4)]
("Dave" "is" "blue" "-")
triple4
Dave is cold.
True
2
proof
[(((triple5) -> rule2))]
("Dave" "is" "cold" "+")
((triple5) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple5) -> rule2))]
("Dave" "is" "cold" "-")
((triple5) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
True
4
proof
[(((((triple5) -> rule2) triple5) -> rule1))]
("Dave" "is" "young" "+")
((((triple5) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not young.
False
4
inv-proof
[(((((triple5) -> rule2) triple5) -> rule1))]
("Dave" "is" "young" "-")
((((triple5) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is kind.
True
5
proof
[(((((((triple5) -> rule2) triple5) -> rule1)) -> rule3))]
("Dave" "is" "kind" "+")
((((((triple5) -> (rule2 % int3)) triple5) -> (rule1 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is not kind.
False
5
inv-proof
[(((((((triple5) -> rule2) triple5) -> rule1)) -> rule3))]
("Dave" "is" "kind" "-")
((((((triple5) -> (rule2 % int3)) triple5) -> (rule1 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "young" "-")
Fiona is kind.
Unknown
rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "young" "-")
Bob is cold.
Unknown
rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "cold" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is kind.[(triple2)] Bob is white.[(triple3)] Dave is blue.[(triple4)] Dave is furry.[(triple5)] Dave is white.[(triple6)] Fiona is cold.[(triple7)] @1: Dave is cold.[(((triple5) -> rule2))] @2: Dave is young.[(((((triple5) -> rule2) triple5) -> rule1))] @3: Dave is kind.[(((((((triple5) -> rule2) triple5) -> rule1)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
Dave is cold.
("Dave" "is" "cold" "+")
((triple5) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple5) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((((triple5) -> (rule2 % int3)) triple5) -> (rule1 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3