Bob is nice. Dave is young. Gary is nice. Harry is round. Blue things are nice. If something is blue and round then it is nice. If something is round then it is furry. If something is nice and furry then it is rough. Round, rough things are blue. Furry things are nice. If Bob is rough then Bob is round. All nice, green things are blue.
Bob is nice.
("Bob" "is" "nice" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
Blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is blue and round then it is nice.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If something is round then it is furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If something is nice and furry then it is rough.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
Round, rough things are blue.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
Furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If Bob is rough then Bob is round.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "round" "+"))
All nice, green things are blue.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Bob is not nice.
False
1
inv-proof
[(triple1)]
("Bob" "is" "nice" "-")
triple1
Harry is furry.
True
2
proof
[(((triple4) -> rule3))]
("Harry" "is" "furry" "+")
((triple4) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple4) -> rule3))]
("Harry" "is" "furry" "-")
((triple4) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
True
3
proof
[(((((triple4) -> rule3)) -> rule6))]
("Harry" "is" "nice" "+")
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule6))]
("Harry" "is" "nice" "-")
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is rough.
True
6
proof
[(((((((triple4) -> rule3)) -> rule6) ((triple4) -> rule3)) -> rule4))]
("Harry" "is" "rough" "+")
((((((triple4) -> (rule3 % int3))) -> (rule6 % int2)) ((triple4) -> (rule3 % int3))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is not rough.
False
6
inv-proof
[(((((((triple4) -> rule3)) -> rule6) ((triple4) -> rule3)) -> rule4))]
("Harry" "is" "rough" "-")
((((((triple4) -> (rule3 % int3))) -> (rule6 % int2)) ((triple4) -> (rule3 % int3))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "furry" "-")
Gary is rough.
Unknown
rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Gary" "is" "rough" "+")
Bob is not rough.
Unknown
inv-rconc
[@3: Bob is rough.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule7 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is round.
Unknown
rconc
[@3: Bob is round.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule3 <- FAIL)]]
("Bob" "is" "round" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Bob is nice.[(triple1)] Dave is young.[(triple2)] Gary is nice.[(triple3)] Harry is round.[(triple4)] @1: Harry is furry.[(((triple4) -> rule3))] @2: Harry is nice.[(((((triple4) -> rule3)) -> rule6))] @3: Harry is rough.[(((((((triple4) -> rule3)) -> rule6) ((triple4) -> rule3)) -> rule4))] @4: Harry is blue.[(((triple4 ((((((triple4) -> rule3)) -> rule6) ((triple4) -> rule3)) -> rule4)) -> rule5))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Harry is furry.
("Harry" "is" "furry" "+")
((triple4) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((((triple4) -> (rule3 % int3))) -> (rule6 % int2)) ((triple4) -> (rule3 % int3))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
((triple4 ((((((triple4) -> (rule3 % int4))) -> (rule6 % int3)) ((triple4) -> (rule3 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4