Anne is not red. Anne is not young. Bob is furry. Bob is white. Gary is not cold. Gary is red. Harry is young. If something is smart then it is young. Young things are big. All big things are cold. If Gary is furry then Gary is young. All red, smart things are white. All cold things are not red. Furry, white things are smart.
Anne is not red.
("Anne" "is" "red" "-")
Anne is not young.
("Anne" "is" "young" "-")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is red.
("Gary" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is smart then it is young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If Gary is furry then Gary is young.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "young" "+"))
All red, smart things are white.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
All cold things are not red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "-"))
Furry, white things are smart.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
Harry is young.
True
1
proof
[(triple7)]
("Harry" "is" "young" "+")
triple7
Harry is not young.
False
1
inv-proof
[(triple7)]
("Harry" "is" "young" "-")
triple7
Harry is big.
True
2
proof
[(((triple7) -> rule2))]
("Harry" "is" "big" "+")
((triple7) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Bob is not smart.
False
3
inv-proof
[(((triple3 triple4) -> rule7))]
("Bob" "is" "smart" "-")
((triple3 triple4) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
True
4
proof
[(((((triple3 triple4) -> rule7)) -> rule1))]
("Bob" "is" "young" "+")
((((triple3 triple4) -> (rule7 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Harry is not cold.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule3))]
("Harry" "is" "cold" "-")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not red.
True
4
proof
[(((((((triple7) -> rule2)) -> rule3)) -> rule6))]
("Harry" "is" "red" "-")
((((((triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is red.
False
4
inv-proof
[(((((((triple7) -> rule2)) -> rule3)) -> rule6))]
("Harry" "is" "red" "+")
((((((triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Bob is cold.
True
6
proof
[(((((((((triple3 triple4) -> rule7)) -> rule1)) -> rule2)) -> rule3))]
("Bob" "is" "cold" "+")
((((((((triple3 triple4) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is not cold.
False
6
inv-proof
[(((((((((triple3 triple4) -> rule7)) -> rule1)) -> rule2)) -> rule3))]
("Bob" "is" "cold" "-")
((((((((triple3 triple4) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is not red.
True
7
proof
[(((((((((((triple3 triple4) -> rule7)) -> rule1)) -> rule2)) -> rule3)) -> rule6))]
("Bob" "is" "red" "-")
((((((((((triple3 triple4) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
Bob is red.
False
7
inv-proof
[(((((((((((triple3 triple4) -> rule7)) -> rule1)) -> rule2)) -> rule3)) -> rule6))]
("Bob" "is" "red" "+")
((((((((((triple3 triple4) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is big.
Unknown
rconc
[@3: Gary is big.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule7 <- FAIL)]]
("Gary" "is" "big" "+")
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "smart" "-")
Gary is white.
Unknown
rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("Gary" "is" "white" "+")
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is cold.
Unknown
rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Anne" "is" "cold" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Anne is not red.[(triple1)] Anne is not young.[(triple2)] Bob is furry.[(triple3)] Bob is white.[(triple4)] Gary is not cold.[(triple5)] Gary is red.[(triple6)] Harry is young.[(triple7)] @1: Bob is smart.[(((triple3 triple4) -> rule7))] Harry is big.[(((triple7) -> rule2))] @2: Bob is young.[(((((triple3 triple4) -> rule7)) -> rule1))] Harry is cold.[(((((triple7) -> rule2)) -> rule3))] @3: Bob is big.[(((((((triple3 triple4) -> rule7)) -> rule1)) -> rule2))] Harry is not red.[(((((((triple7) -> rule2)) -> rule3)) -> rule6))] @4: Bob is cold.[(((((((((triple3 triple4) -> rule7)) -> rule1)) -> rule2)) -> rule3))] @5: Bob is not red.[(((((((((((triple3 triple4) -> rule7)) -> rule1)) -> rule2)) -> rule3)) -> rule6))]
Anne is not red.
("Anne" "is" "red" "-")
triple1
Anne is not young.
("Anne" "is" "young" "-")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Gary is not cold.
("Gary" "is" "cold" "-")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
((triple3 triple4) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple7) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple3 triple4) -> (rule7 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((((triple3 triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Harry is not red.
("Harry" "is" "red" "-")
((((((triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((((((((triple3 triple4) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is not red.
("Bob" "is" "red" "-")
((((((((((triple3 triple4) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5