Bob is big. Dave is big. Gary is furry. If someone is cold then they are furry. Cold people are furry. All furry people are young. If Gary is green and Gary is red then Gary is young. All green, young people are cold. All young, furry people are green.
Bob is big.
("Bob" "is" "big" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
If someone is cold then they are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
All furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If Gary is green and Gary is red then Gary is young.
((("Gary" "is" "green" "+") ("Gary" "is" "red" "+")) -> ("Gary" "is" "young" "+"))
All green, young people are cold.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
All young, furry people are green.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Dave is not big.
False
1
inv-proof
[(triple2)]
("Dave" "is" "big" "-")
triple2
Gary is young.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "young" "+")
((triple3) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "young" "-")
((triple3) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
True
4
proof
[(((((triple3) -> rule3) triple3) -> rule6))]
("Gary" "is" "green" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not green.
False
4
inv-proof
[(((((triple3) -> rule3) triple3) -> rule6))]
("Gary" "is" "green" "-")
((((triple3) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is cold.
True
7
proof
[(((((((triple3) -> rule3) triple3) -> rule6) ((triple3) -> rule3)) -> rule5))]
("Gary" "is" "cold" "+")
((((((triple3) -> (rule3 % int3)) triple3) -> (rule6 % int2)) ((triple3) -> (rule3 % int3))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is not cold.
False
7
inv-proof
[(((((((triple3) -> rule3) triple3) -> rule6) ((triple3) -> rule3)) -> rule5))]
("Gary" "is" "cold" "-")
((((((triple3) -> (rule3 % int3)) triple3) -> (rule6 % int2)) ((triple3) -> (rule3 % int3))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Bob is not cold.
Unknown
inv-rconc
[@3: Bob is cold.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule1 <- FAIL)]]
("Bob" "is" "cold" "-")
Dave is young.
Unknown
rconc
[@3: Dave is young.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule5 <- FAIL)]]
("Dave" "is" "young" "+")
Dave is not furry.
Unknown
inv-rconc
[@4: Dave is furry.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule6 <- rule2 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is cold.
Unknown
rconc
[@3: Dave is cold.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule1 <- FAIL)]]
("Dave" "is" "cold" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Bob is big.[(triple1)] Dave is big.[(triple2)] Gary is furry.[(triple3)] @1: Gary is young.[(((triple3) -> rule3))] @2: Gary is green.[(((((triple3) -> rule3) triple3) -> rule6))] @3: Gary is cold.[(((((((triple3) -> rule3) triple3) -> rule6) ((triple3) -> rule3)) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Gary is young.
("Gary" "is" "young" "+")
((triple3) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple3) -> (rule3 % int3)) triple3) -> (rule6 % int2)) ((triple3) -> (rule3 % int3))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3