Bob is quiet. Gary is big. Gary is nice. Gary is quiet. Gary is rough. Harry is big. Harry is blue. Harry is nice. Harry is quiet. Harry is rough. Harry is white. Harry is young. All white, quiet people are blue. If someone is rough then they are big. If Harry is young then Harry is nice. Nice, quiet people are young. If someone is young and blue then they are nice. All rough, white people are big. Young, nice people are white. Big people are rough.
Bob is quiet.
("Bob" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
All white, quiet people are blue.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough then they are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If Harry is young then Harry is nice.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "nice" "+"))
Nice, quiet people are young.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If someone is young and blue then they are nice.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
All rough, white people are big.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Young, nice people are white.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
Big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Gary is nice.
True
1
proof
[(triple3)]
("Gary" "is" "nice" "+")
triple3
Harry is not quiet.
False
1
inv-proof
[(triple9)]
("Harry" "is" "quiet" "-")
triple9
Gary is young.
True
3
proof
[(((triple3 triple4) -> rule4))]
("Gary" "is" "young" "+")
((triple3 triple4) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not young.
False
3
inv-proof
[(((triple3 triple4) -> rule4))]
("Gary" "is" "young" "-")
((triple3 triple4) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Bob is not white.
Unknown
inv-rconc
[@3: Bob is white.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule5 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is nice.
Unknown
rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is quiet.[(triple1)] Gary is big.[(triple2 OR ((triple5) -> rule2) OR ((triple5 ((((triple3 triple4) -> rule4) triple3) -> rule7)) -> rule6))] Gary is nice.[(triple3)] Gary is quiet.[(triple4)] Gary is rough.[(triple5 OR ((triple2) -> rule8))] Harry is big.[(triple6 OR ((triple10) -> rule2) OR ((triple10 triple11) -> rule6) OR ((triple10 ((triple12 triple8) -> rule7)) -> rule6) OR ((triple10 ((triple12 ((triple12) -> rule3)) -> rule7)) -> rule6) OR ((triple10 ((triple12 ((triple12 triple7) -> rule5)) -> rule7)) -> rule6) OR ((triple10 ((((triple8 triple9) -> rule4) triple8) -> rule7)) -> rule6) OR ((triple10 ((((triple8 triple9) -> rule4) ((triple12) -> rule3)) -> rule7)) -> rule6) OR ((triple10 ((((triple8 triple9) -> rule4) ((triple12 triple7) -> rule5)) -> rule7)) -> rule6))] Harry is blue.[(triple7 OR ((triple11 triple9) -> rule1) OR ((((triple12 triple8) -> rule7) triple9) -> rule1) OR ((((triple12 ((triple12) -> rule3)) -> rule7) triple9) -> rule1) OR ((((((triple8 triple9) -> rule4) triple8) -> rule7) triple9) -> rule1) OR ((((((triple8 triple9) -> rule4) ((triple12) -> rule3)) -> rule7) triple9) -> rule1))] Harry is nice.[(triple8 OR ((triple12) -> rule3) OR ((triple12 triple7) -> rule5) OR ((triple12 ((triple11 triple9) -> rule1)) -> rule5))] Harry is quiet.[(triple9)] Harry is rough.[(triple10 OR ((triple6) -> rule8))] Harry is white.[(triple11 OR ((triple12 triple8) -> rule7) OR ((triple12 ((triple12) -> rule3)) -> rule7) OR ((triple12 ((triple12 triple7) -> rule5)) -> rule7) OR ((((triple8 triple9) -> rule4) triple8) -> rule7) OR ((((triple8 triple9) -> rule4) ((triple12) -> rule3)) -> rule7) OR ((((triple8 triple9) -> rule4) ((triple12 triple7) -> rule5)) -> rule7))] Harry is young.[(triple12 OR ((triple8 triple9) -> rule4))] @1: Gary is young.[(((triple3 triple4) -> rule4))] @2: Gary is white.[(((((triple3 triple4) -> rule4) triple3) -> rule7))] @3: Gary is blue.[(((((((triple3 triple4) -> rule4) triple3) -> rule7) triple4) -> rule1))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Gary is big.
("Gary" "is" "big" "+")
triple2
((triple5) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple5 ((((triple3 triple4) -> (rule4 % int3)) triple3) -> (rule7 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple5
((triple2) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple6
((triple10) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple10 triple11) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple10 ((triple12 triple8) -> (rule7 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((triple10 ((triple12 ((triple12) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((triple10 ((triple12 ((triple12 triple7) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((triple10 ((((triple8 triple9) -> (rule4 % int3)) triple8) -> (rule7 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((triple10 ((((triple8 triple9) -> (rule4 % int4)) ((triple12) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
((triple10 ((((triple8 triple9) -> (rule4 % int4)) ((triple12 triple7) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is blue.
("Harry" "is" "blue" "+")
triple7
((triple11 triple9) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple12 triple8) -> (rule7 % int2)) triple9) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple12 ((triple12) -> (rule3 % int3))) -> (rule7 % int2)) triple9) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple8 triple9) -> (rule4 % int3)) triple8) -> (rule7 % int2)) triple9) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((((triple8 triple9) -> (rule4 % int4)) ((triple12) -> (rule3 % int3))) -> (rule7 % int2)) triple9) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple12) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple12 triple7) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple12 ((triple11 triple9) -> (rule1 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
((triple6) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple11
((triple12 triple8) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple12 ((triple12) -> (rule3 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple12 ((triple12 triple7) -> (rule5 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple8 triple9) -> (rule4 % int2)) triple8) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple8 triple9) -> (rule4 % int3)) ((triple12) -> (rule3 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((triple8 triple9) -> (rule4 % int3)) ((triple12 triple7) -> (rule5 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
triple12
((triple8 triple9) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple3 triple4) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple3 triple4) -> (rule4 % int2)) triple3) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple3 triple4) -> (rule4 % int3)) triple3) -> (rule7 % int2)) triple4) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3