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