Bob is big. Bob is nice. Bob is quiet. Bob is red. Bob is rough. Bob is young. Harry is not big. Harry is not nice. Harry is rough. Harry is not white. If something is red and not nice then it is young. All young, red things are rough. Rough things are red.
Bob is big.
("Bob" "is" "big" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not white.
("Harry" "is" "white" "-")
If something is red and not nice then it is young.
((("something" "is" "red" "+") ("something" "is" "nice" "~")) -> ("something" "is" "young" "+"))
All young, red things are rough.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
Bob is rough.
True
1
proof
[(triple5 OR ((triple6 triple4) -> rule2))]
("Bob" "is" "rough" "+")
triple5
((triple6 triple4) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not quiet.
False
1
inv-proof
[(triple3)]
("Bob" "is" "quiet" "-")
triple3
Harry is red.
True
2
proof
[(((triple9) -> rule3))]
("Harry" "is" "red" "+")
((triple9) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple9) -> rule3))]
("Harry" "is" "red" "-")
((triple9) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
True
4
proof
[(((((triple9) -> rule3) triple8) -> rule1))]
("Harry" "is" "young" "+")
((((triple9) -> (rule3 % int2)) triple8) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not young.
False
4
inv-proof
[(((((triple9) -> rule3) triple8) -> rule1))]
("Harry" "is" "young" "-")
((((triple9) -> (rule3 % int2)) triple8) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is big.[(triple1)] Bob is nice.[(triple2)] Bob is quiet.[(triple3)] Bob is red.[(triple4 OR ((triple5) -> rule3))] Bob is rough.[(triple5 OR ((triple6 triple4) -> rule2))] Bob is young.[(triple6)] Harry is not big.[(triple7)] Harry is not nice.[(triple8)] Harry is not white.[(triple10)] Harry is rough.[(triple9)] @1: Harry is red.[(((triple9) -> rule3))] @2: Harry is young.[(((((triple9) -> rule3) triple8) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple5) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple6 triple4) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple6
Harry is not big.
("Harry" "is" "big" "-")
triple7
Harry is not nice.
("Harry" "is" "nice" "-")
triple8
Harry is not white.
("Harry" "is" "white" "-")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
((triple9) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple9) -> (rule3 % int2)) triple8) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2