Anne is smart. Bob is young. Gary is not big. Harry is young. Cold people are not white. Young people are cold. If Gary is red and Gary is white then Gary is green. Red people are young. Smart people are red. If Anne is smart and Anne is not big then Anne is red.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is not big.
("Gary" "is" "big" "-")
Harry is young.
("Harry" "is" "young" "+")
Cold people are not white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "-"))
Young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If Gary is red and Gary is white then Gary is green.
((("Gary" "is" "red" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "green" "+"))
Red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Smart people are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If Anne is smart and Anne is not big then Anne is red.
((("Anne" "is" "smart" "+") ("Anne" "is" "big" "~")) -> ("Anne" "is" "red" "+"))
Bob is young.
True
1
proof
[(triple2)]
("Bob" "is" "young" "+")
triple2
Harry is not young.
False
1
inv-proof
[(triple4)]
("Harry" "is" "young" "-")
triple4
Bob is cold.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Anne is not red.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "red" "-")
((triple1) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
True
3
proof
[(((((triple1) -> rule5)) -> rule4))]
("Anne" "is" "young" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Bob is white.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "white" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is young.
Unknown
rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Gary" "is" "young" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Anne is smart.[(triple1)] Bob is young.[(triple2)] Gary is not big.[(triple3)] Harry is young.[(triple4)] @1: Anne is red.[(((triple1) -> rule5))] Bob is cold.[(((triple2) -> rule2))] Harry is cold.[(((triple4) -> rule2))] @2: Anne is young.[(((((triple1) -> rule5)) -> rule4))] Bob is not white.[(((((triple2) -> rule2)) -> rule1))] Harry is not white.[(((((triple4) -> rule2)) -> rule1))] @3: Anne is cold.[(((((((triple1) -> rule5)) -> rule4)) -> rule2))] @4: Anne is not white.[(((((((((triple1) -> rule5)) -> rule4)) -> rule2)) -> rule1))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Gary is not big.
("Gary" "is" "big" "-")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Bob is not white.
("Bob" "is" "white" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Harry is not white.
("Harry" "is" "white" "-")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is not white.
("Anne" "is" "white" "-")
((((((((triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4