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