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