Bob is furry. Bob is green. Bob is quiet. Bob is smart. Bob is young. Charlie is blue. Charlie is green. Charlie is quiet. Charlie is round. Charlie is young. Gary is furry. Gary is smart. Gary is young. Harry is quiet. Harry is young. Smart things are green. If something is green then it is furry. If something is young then it is smart.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is green then it is furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
If something is young then it is smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
Charlie is young.
True
1
proof
[(triple10)]
("Charlie" "is" "young" "+")
triple10
Gary is not young.
False
1
inv-proof
[(triple13)]
("Gary" "is" "young" "-")
triple13
Charlie is furry.
True
2
proof
[(((triple7) -> rule2) OR ((((((triple10) -> rule3)) -> rule1)) -> rule2))]
("Charlie" "is" "furry" "+")
((triple7) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((((triple10) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Gary is not green.
False
2
inv-proof
[(((triple12) -> rule1) OR ((((triple13) -> rule3)) -> rule1))]
("Gary" "is" "green" "-")
((triple12) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple13) -> (rule3 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Harry is green.
True
3
proof
[(((((triple15) -> rule3)) -> rule1))]
("Harry" "is" "green" "+")
((((triple15) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not green.
False
3
inv-proof
[(((((triple15) -> rule3)) -> rule1))]
("Harry" "is" "green" "-")
((((triple15) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is furry.
True
4
proof
[(((((((triple15) -> rule3)) -> rule1)) -> rule2))]
("Harry" "is" "furry" "+")
((((((triple15) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not furry.
False
4
inv-proof
[(((((((triple15) -> rule3)) -> rule1)) -> rule2))]
("Harry" "is" "furry" "-")
((((((triple15) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is furry.[(triple1 OR ((triple2) -> rule2) OR ((((triple4) -> rule1)) -> rule2) OR ((((((triple5) -> rule3)) -> rule1)) -> rule2))] Bob is green.[(triple2 OR ((triple4) -> rule1) OR ((((triple5) -> rule3)) -> rule1))] Bob is quiet.[(triple3)] Bob is smart.[(triple4 OR ((triple5) -> rule3))] Bob is young.[(triple5)] Charlie is blue.[(triple6)] Charlie is green.[(triple7 OR ((((triple10) -> rule3)) -> rule1))] Charlie is quiet.[(triple8)] Charlie is round.[(triple9)] Charlie is young.[(triple10)] Gary is furry.[(triple11 OR ((((triple12) -> rule1)) -> rule2) OR ((((((triple13) -> rule3)) -> rule1)) -> rule2))] Gary is smart.[(triple12 OR ((triple13) -> rule3))] Gary is young.[(triple13)] Harry is quiet.[(triple14)] Harry is young.[(triple15)] @1: Charlie is furry.[(((triple7) -> rule2) OR ((((((triple10) -> rule3)) -> rule1)) -> rule2))] Charlie is smart.[(((triple10) -> rule3))] Gary is green.[(((triple12) -> rule1) OR ((((triple13) -> rule3)) -> rule1))] Harry is smart.[(((triple15) -> rule3))] @2: Harry is green.[(((((triple15) -> rule3)) -> rule1))] @3: Harry is furry.[(((((((triple15) -> rule3)) -> rule1)) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
((triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple4) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
((triple5) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple5
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
Charlie is round.
("Charlie" "is" "round" "+")
triple9
Charlie is young.
("Charlie" "is" "young" "+")
triple10
Gary is furry.
("Gary" "is" "furry" "+")
triple11
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((((triple13) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
triple12
((triple13) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple7) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((((triple10) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple10) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple12) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple13) -> (rule3 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((triple15) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple15) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((((triple15) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3