Bob is cold. Bob is round. Dave is cold. Dave is young. Gary is cold. Gary is furry. Gary is nice. Gary is round. Gary is young. Harry is cold. Harry is furry. Harry is round. If something is young and furry then it is round. If something is round then it is red. Young things are furry. Nice, young things are cold. If Harry is red then Harry is white. If Dave is furry and Dave is white then Dave is round. All young, nice things are white. All round, red things are furry.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is young and furry then it is round.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Nice, young things are cold.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If Harry is red then Harry is white.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "white" "+"))
If Dave is furry and Dave is white then Dave is round.
((("Dave" "is" "furry" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "round" "+"))
All young, nice things are white.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
All round, red things are furry.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Gary is young.
True
1
proof
[(triple9)]
("Gary" "is" "young" "+")
triple9
Gary is not nice.
False
1
inv-proof
[(triple7)]
("Gary" "is" "nice" "-")
triple7
Gary is white.
True
3
proof
[(((triple9 triple7) -> rule7))]
("Gary" "is" "white" "+")
((triple9 triple7) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
3
inv-proof
[(((triple9 triple7) -> rule7))]
("Gary" "is" "white" "-")
((triple9 triple7) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is round.
True
4
proof
[(((triple4 ((triple4) -> rule3)) -> rule1))]
("Dave" "is" "round" "+")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Harry is not white.
False
3
inv-proof
[(((((triple12) -> rule2)) -> rule5))]
("Harry" "is" "white" "-")
((((triple12) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Dave is red.
True
5
proof
[(((((triple4 ((triple4) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "red" "+")
((((triple4 ((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not red.
False
5
inv-proof
[(((((triple4 ((triple4) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "red" "-")
((((triple4 ((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "white" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "white" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Bob is cold.[(triple1)] Bob is round.[(triple2)] Dave is cold.[(triple3)] Dave is young.[(triple4)] Gary is cold.[(triple5 OR ((triple7 triple9) -> rule4))] Gary is furry.[(triple6 OR ((triple9) -> rule3) OR ((triple8 ((triple8) -> rule2)) -> rule8))] Gary is nice.[(triple7)] Gary is round.[(triple8 OR ((triple9 triple6) -> rule1) OR ((triple9 ((triple9) -> rule3)) -> rule1))] Gary is young.[(triple9)] Harry is cold.[(triple10)] Harry is furry.[(triple11 OR ((triple12 ((triple12) -> rule2)) -> rule8))] Harry is round.[(triple12)] @1: Bob is red.[(((triple2) -> rule2))] Dave is furry.[(((triple4) -> rule3))] Gary is red.[(((triple8) -> rule2) OR ((((triple9 triple6) -> rule1)) -> rule2) OR ((((triple9 ((triple9) -> rule3)) -> rule1)) -> rule2))] Gary is white.[(((triple9 triple7) -> rule7))] Harry is red.[(((triple12) -> rule2))] @2: Bob is furry.[(((triple2 ((triple2) -> rule2)) -> rule8))] Dave is round.[(((triple4 ((triple4) -> rule3)) -> rule1))] Harry is white.[(((((triple12) -> rule2)) -> rule5))] @3: Dave is red.[(((((triple4 ((triple4) -> rule3)) -> rule1)) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
((triple7 triple9) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple6
((triple9) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple8 ((triple8) -> (rule2 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple7
Gary is round.
("Gary" "is" "round" "+")
triple8
((triple9 triple6) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple9 ((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
((triple12 ((triple12) -> (rule2 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple12
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple4) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple8) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple9 triple6) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple9 ((triple9) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((triple9 triple7) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple12) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple12) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple4 ((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3