Bob is furry. Bob is red. Charlie is nice. Charlie is quiet. Charlie is round. Charlie is smart. Harry is furry. Harry is quiet. Harry is red. Harry is round. All furry things are smart. All smart, big things are quiet. Smart things are big.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
All furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
All smart, big things are quiet.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Harry is furry.
True
1
proof
[(triple7)]
("Harry" "is" "furry" "+")
triple7
Bob is not red.
False
1
inv-proof
[(triple2)]
("Bob" "is" "red" "-")
triple2
Bob is smart.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple6) -> rule3))]
("Charlie" "is" "big" "-")
((triple6) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Harry is big.
True
3
proof
[(((((triple7) -> rule1)) -> rule3))]
("Harry" "is" "big" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Bob is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Bob" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
True
6
proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule2))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not quiet.
False
6
inv-proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule2))]
("Bob" "is" "quiet" "-")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Bob is furry.[(triple1)] Bob is red.[(triple2)] Charlie is nice.[(triple3)] Charlie is quiet.[(triple4 OR ((triple6 ((triple6) -> rule3)) -> rule2))] Charlie is round.[(triple5)] Charlie is smart.[(triple6)] Harry is furry.[(triple7)] Harry is quiet.[(triple8 OR ((((triple7) -> rule1) ((((triple7) -> rule1)) -> rule3)) -> rule2))] Harry is red.[(triple9)] Harry is round.[(triple10)] @1: Bob is smart.[(((triple1) -> rule1))] Charlie is big.[(((triple6) -> rule3))] Harry is smart.[(((triple7) -> rule1))] @2: Bob is big.[(((((triple1) -> rule1)) -> rule3))] Harry is big.[(((((triple7) -> rule1)) -> rule3))] @3: Bob is quiet.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
((triple6 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
((((triple7) -> (rule1 % int3)) ((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple6) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple7) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3