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