Bob is not blue. Dave is young. Gary is cold. Harry is not round. All cold, young people are nice. Young people are cold. If Harry is round and Harry is not young then Harry is furry. Big, nice people are not furry. If Dave is round then Dave is not blue. Nice people are big.
Bob is not blue.
("Bob" "is" "blue" "-")
Dave is young.
("Dave" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is not round.
("Harry" "is" "round" "-")
All cold, young people are nice.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If Harry is round and Harry is not young then Harry is furry.
((("Harry" "is" "round" "+") ("Harry" "is" "young" "~")) -> ("Harry" "is" "furry" "+"))
Big, nice people are not furry.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "-"))
If Dave is round then Dave is not blue.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "blue" "-"))
Nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Dave is young.
True
1
proof
[(triple2)]
("Dave" "is" "young" "+")
triple2
Bob is blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Dave is cold.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "cold" "-")
((triple2) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
True
4
proof
[(((((triple2) -> rule2) triple2) -> rule1))]
("Dave" "is" "nice" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not nice.
False
4
inv-proof
[(((((triple2) -> rule2) triple2) -> rule1))]
("Dave" "is" "nice" "-")
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is big.
True
5
proof
[(((((((triple2) -> rule2) triple2) -> rule1)) -> rule6))]
("Dave" "is" "big" "+")
((((((triple2) -> (rule2 % int3)) triple2) -> (rule1 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is not big.
False
5
inv-proof
[(((((((triple2) -> rule2) triple2) -> rule1)) -> rule6))]
("Dave" "is" "big" "-")
((((((triple2) -> (rule2 % int3)) triple2) -> (rule1 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is big.
Unknown
rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Bob" "is" "big" "+")
Gary is not big.
Unknown
inv-rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Gary" "is" "big" "-")
Harry is big.
Unknown
rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Harry" "is" "big" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Bob is not blue.[(triple1)] Dave is young.[(triple2)] Gary is cold.[(triple3)] Harry is not round.[(triple4)] @1: Dave is cold.[(((triple2) -> rule2))] @2: Dave is nice.[(((((triple2) -> rule2) triple2) -> rule1))] @3: Dave is big.[(((((((triple2) -> rule2) triple2) -> rule1)) -> rule6))] @4: Dave is not furry.[(((((((((triple2) -> rule2) triple2) -> rule1)) -> rule6) ((((triple2) -> rule2) triple2) -> rule1)) -> rule4))]
Bob is not blue.
("Bob" "is" "blue" "-")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Harry is not round.
("Harry" "is" "round" "-")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple2) -> (rule2 % int3)) triple2) -> (rule1 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is not furry.
("Dave" "is" "furry" "-")
((((((((triple2) -> (rule2 % int4)) triple2) -> (rule1 % int3))) -> (rule6 % int2)) ((((triple2) -> (rule2 % int4)) triple2) -> (rule1 % int3))) -> (rule4 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4