Anne is rough. Anne is round. Bob is white. Gary is blue. Gary is cold. Gary is green. Harry is green. Blue, cold people are rough. If someone is blue then they are cold. If someone is white and young then they are cold. White, round people are blue. All rough people are not young. All young, rough people are not green. If someone is white then they are round. Young, blue people are white.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Harry is green.
("Harry" "is" "green" "+")
Blue, cold people are rough.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue then they are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If someone is white and young then they are cold.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
White, round people are blue.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
All rough people are not young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "-"))
All young, rough people are not green.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "-"))
If someone is white then they are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
Young, blue people are white.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Harry is green.
True
1
proof
[(triple7)]
("Harry" "is" "green" "+")
triple7
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Bob is round.
True
2
proof
[(((triple3) -> rule7))]
("Bob" "is" "round" "+")
((triple3) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple3) -> rule7))]
("Bob" "is" "round" "-")
((triple3) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Gary is not young.
True
4
proof
[(((((triple4 triple5) -> rule1)) -> rule5) OR ((((triple4 ((triple4) -> rule2)) -> rule1)) -> rule5))]
("Gary" "is" "young" "-")
((((triple4 triple5) -> (rule1 % int2))) -> (rule5 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple4 ((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is young.
False
4
inv-proof
[(((((triple4 triple5) -> rule1)) -> rule5) OR ((((triple4 ((triple4) -> rule2)) -> rule1)) -> rule5))]
("Gary" "is" "young" "+")
((((triple4 triple5) -> (rule1 % int2))) -> (rule5 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple4 ((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Bob is cold.
True
5
proof
[(((((triple3 ((triple3) -> rule7)) -> rule4)) -> rule2))]
("Bob" "is" "cold" "+")
((((triple3 ((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not cold.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule7)) -> rule4)) -> rule2))]
("Bob" "is" "cold" "-")
((((triple3 ((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is rough.
True
10
proof
[(((((triple3 ((triple3) -> rule7)) -> rule4) ((((triple3 ((triple3) -> rule7)) -> rule4)) -> rule2)) -> rule1))]
("Bob" "is" "rough" "+")
((((triple3 ((triple3) -> (rule7 % int4))) -> (rule4 % int3)) ((((triple3 ((triple3) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is not rough.
False
10
inv-proof
[(((((triple3 ((triple3) -> rule7)) -> rule4) ((((triple3 ((triple3) -> rule7)) -> rule4)) -> rule2)) -> rule1))]
("Bob" "is" "rough" "-")
((((triple3 ((triple3) -> (rule7 % int4))) -> (rule4 % int3)) ((((triple3 ((triple3) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is not young.
True
11
proof
[(((((((triple3 ((triple3) -> rule7)) -> rule4) ((((triple3 ((triple3) -> rule7)) -> rule4)) -> rule2)) -> rule1)) -> rule5))]
("Bob" "is" "young" "-")
((((((triple3 ((triple3) -> (rule7 % int5))) -> (rule4 % int4)) ((((triple3 ((triple3) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5
Bob is young.
False
11
inv-proof
[(((((((triple3 ((triple3) -> rule7)) -> rule4) ((((triple3 ((triple3) -> rule7)) -> rule4)) -> rule2)) -> rule1)) -> rule5))]
("Bob" "is" "young" "+")
((((((triple3 ((triple3) -> (rule7 % int5))) -> (rule4 % int4)) ((((triple3 ((triple3) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5
Anne is not blue.
Unknown
inv-rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Anne" "is" "blue" "-")
Gary is round.
Unknown
rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("Gary" "is" "round" "+")
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is cold.
Unknown
rconc
[@3: Harry is cold.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule8 <- FAIL)]]
("Harry" "is" "cold" "+")
Harry is not blue.
Unknown
inv-rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Harry" "is" "blue" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "white" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Anne is rough.[(triple1)] Anne is round.[(triple2)] Bob is white.[(triple3)] Gary is blue.[(triple4)] Gary is cold.[(triple5 OR ((triple4) -> rule2))] Gary is green.[(triple6)] Harry is green.[(triple7)] @1: Anne is not young.[(((triple1) -> rule5))] Bob is round.[(((triple3) -> rule7))] Gary is rough.[(((triple4 triple5) -> rule1) OR ((triple4 ((triple4) -> rule2)) -> rule1))] @2: Bob is blue.[(((triple3 ((triple3) -> rule7)) -> rule4))] Gary is not young.[(((((triple4 triple5) -> rule1)) -> rule5) OR ((((triple4 ((triple4) -> rule2)) -> rule1)) -> rule5))] @3: Bob is cold.[(((((triple3 ((triple3) -> rule7)) -> rule4)) -> rule2))] @4: Bob is rough.[(((((triple3 ((triple3) -> rule7)) -> rule4) ((((triple3 ((triple3) -> rule7)) -> rule4)) -> rule2)) -> rule1))] @5: Bob is not young.[(((((((triple3 ((triple3) -> rule7)) -> rule4) ((((triple3 ((triple3) -> rule7)) -> rule4)) -> rule2)) -> rule1)) -> rule5))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
((triple4) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Anne is not young.
("Anne" "is" "young" "-")
((triple1) -> (rule5 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple3) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple4 triple5) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple4 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((triple3 ((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Gary is not young.
("Gary" "is" "young" "-")
((((triple4 triple5) -> (rule1 % int2))) -> (rule5 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple4 ((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((((triple3 ((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((triple3 ((triple3) -> (rule7 % int4))) -> (rule4 % int3)) ((((triple3 ((triple3) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is not young.
("Bob" "is" "young" "-")
((((((triple3 ((triple3) -> (rule7 % int5))) -> (rule4 % int4)) ((((triple3 ((triple3) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5