Bob is big. Bob is quiet. Bob is round. Dave is round. Dave is white. Dave is young. Harry is big. Harry is not green. Harry is nice. Harry is not round. Harry is white. Harry is young. Nice, quiet things are not green. If Harry is nice and Harry is round then Harry is big. If something is round and not young then it is big. If something is quiet and white then it is nice. Big things are white. If Dave is round then Dave is nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not green.
("Harry" "is" "green" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not round.
("Harry" "is" "round" "-")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
Nice, quiet things are not green.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "-"))
If Harry is nice and Harry is round then Harry is big.
((("Harry" "is" "nice" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "big" "+"))
If something is round and not young then it is big.
((("something" "is" "round" "+") ("something" "is" "young" "~")) -> ("something" "is" "big" "+"))
If something is quiet and white then it is nice.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If Dave is round then Dave is nice.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "nice" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Harry is not white.
False
1
inv-proof
[(triple11 OR ((triple7) -> rule5))]
("Harry" "is" "white" "-")
triple11
((triple7) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Bob is white.
True
2
proof
[(((triple1) -> rule5))]
("Bob" "is" "white" "+")
((triple1) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple4) -> rule6))]
("Dave" "is" "nice" "-")
((triple4) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Bob is nice.
True
4
proof
[(((triple2 ((triple1) -> rule5)) -> rule4))]
("Bob" "is" "nice" "+")
((triple2 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not nice.
False
4
inv-proof
[(((triple2 ((triple1) -> rule5)) -> rule4))]
("Bob" "is" "nice" "-")
((triple2 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not green.
True
6
proof
[(((((triple2 ((triple1) -> rule5)) -> rule4) triple2) -> rule1))]
("Bob" "is" "green" "-")
((((triple2 ((triple1) -> (rule5 % int3))) -> (rule4 % int2)) triple2) -> (rule1 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is green.
False
6
inv-proof
[(((((triple2 ((triple1) -> rule5)) -> rule4) triple2) -> rule1))]
("Bob" "is" "green" "+")
((((triple2 ((triple1) -> (rule5 % int3))) -> (rule4 % int2)) triple2) -> (rule1 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "big" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
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 round.[(triple3)] Dave is round.[(triple4)] Dave is white.[(triple5)] Dave is young.[(triple6)] Harry is big.[(triple7)] Harry is nice.[(triple9)] Harry is not green.[(triple8)] Harry is not round.[(triple10)] Harry is white.[(triple11 OR ((triple7) -> rule5))] Harry is young.[(triple12)] @1: Bob is white.[(((triple1) -> rule5))] Dave is nice.[(((triple4) -> rule6))] @2: Bob is nice.[(((triple2 ((triple1) -> rule5)) -> rule4))] @3: Bob is not green.[(((((triple2 ((triple1) -> rule5)) -> rule4) triple2) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is not green.
("Harry" "is" "green" "-")
triple8
Harry is not round.
("Harry" "is" "round" "-")
triple10
Harry is white.
("Harry" "is" "white" "+")
triple11
((triple7) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple12
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple4) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple2 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not green.
("Bob" "is" "green" "-")
((((triple2 ((triple1) -> (rule5 % int3))) -> (rule4 % int2)) triple2) -> (rule1 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3