Bob is big. Bob is quiet. Bob is smart. Dave is big. Dave is smart. Dave is white. Harry is big. Harry is kind. Harry is smart. Harry is white. Big people are green. All round people are kind. Big, green people are round.
Bob is big.
("Bob" "is" "big" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Big, green people are round.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Harry is white.
True
1
proof
[(triple10)]
("Harry" "is" "white" "+")
triple10
Harry is not big.
False
1
inv-proof
[(triple7)]
("Harry" "is" "big" "-")
triple7
Bob is green.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "green" "+")
((triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple4) -> rule1))]
("Dave" "is" "green" "-")
((triple4) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
True
4
proof
[(((triple4 ((triple4) -> rule1)) -> rule3))]
("Dave" "is" "round" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not round.
False
4
inv-proof
[(((triple4 ((triple4) -> rule1)) -> rule3))]
("Dave" "is" "round" "-")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Bob is kind.
True
5
proof
[(((((triple1 ((triple1) -> rule1)) -> rule3)) -> rule2))]
("Bob" "is" "kind" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Dave is not kind.
False
5
inv-proof
[(((((triple4 ((triple4) -> rule1)) -> rule3)) -> rule2))]
("Dave" "is" "kind" "-")
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Bob is big.[(triple1)] Bob is quiet.[(triple2)] Bob is smart.[(triple3)] Dave is big.[(triple4)] Dave is smart.[(triple5)] Dave is white.[(triple6)] Harry is big.[(triple7)] Harry is kind.[(triple8 OR ((((triple7 ((triple7) -> rule1)) -> rule3)) -> rule2))] Harry is smart.[(triple9)] Harry is white.[(triple10)] @1: Bob is green.[(((triple1) -> rule1))] Dave is green.[(((triple4) -> rule1))] Harry is green.[(((triple7) -> rule1))] @2: Bob is round.[(((triple1 ((triple1) -> rule1)) -> rule3))] Dave is round.[(((triple4 ((triple4) -> rule1)) -> rule3))] Harry is round.[(((triple7 ((triple7) -> rule1)) -> rule3))] @3: Bob is kind.[(((((triple1 ((triple1) -> rule1)) -> rule3)) -> rule2))] Dave is kind.[(((((triple4 ((triple4) -> rule1)) -> rule3)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple8
((((triple7 ((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple4) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple7) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3