Anne is not blue. Anne is cold. Anne is smart. Erin is smart. Erin is white. Erin is young. Gary is blue. Gary is quiet. Harry is not cold. Harry is quiet. Harry is rough. Harry is smart. Rough people are young. Blue people are not white. If someone is smart and not blue then they are white. White people are rough. If Erin is smart then Erin is rough. If Erin is not white and Erin is not young then Erin is not quiet. If Anne is not blue and Anne is not white then Anne is quiet. If Anne is white and Anne is not cold then Anne is not quiet.
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
Blue people are not white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "-"))
If someone is smart and not blue then they are white.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "white" "+"))
White people are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If Erin is smart then Erin is rough.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "rough" "+"))
If Erin is not white and Erin is not young then Erin is not quiet.
((("Erin" "is" "white" "~") ("Erin" "is" "young" "~")) -> ("Erin" "is" "quiet" "-"))
If Anne is not blue and Anne is not white then Anne is quiet.
((("Anne" "is" "blue" "~") ("Anne" "is" "white" "~")) -> ("Anne" "is" "quiet" "+"))
If Anne is white and Anne is not cold then Anne is not quiet.
((("Anne" "is" "white" "+") ("Anne" "is" "cold" "~")) -> ("Anne" "is" "quiet" "-"))
Anne is cold.
True
1
proof
[(triple2)]
("Anne" "is" "cold" "+")
triple2
Harry is cold.
False
1
inv-proof
[(triple9)]
("Harry" "is" "cold" "+")
triple9
Gary is not white.
True
2
proof
[(((triple7) -> rule2))]
("Gary" "is" "white" "-")
((triple7) -> (rule2 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Harry is not young.
False
2
inv-proof
[(((triple11) -> rule1))]
("Harry" "is" "young" "-")
((triple11) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is rough.
True
4
proof
[(((((triple3 triple1) -> rule3)) -> rule4))]
("Anne" "is" "rough" "+")
((((triple3 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not rough.
False
4
inv-proof
[(((((triple3 triple1) -> rule3)) -> rule4))]
("Anne" "is" "rough" "-")
((((triple3 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
True
5
proof
[(((((((triple3 triple1) -> rule3)) -> rule4)) -> rule1))]
("Anne" "is" "young" "+")
((((((triple3 triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not young.
False
5
inv-proof
[(((((((triple3 triple1) -> rule3)) -> rule4)) -> rule1))]
("Anne" "is" "young" "-")
((((((triple3 triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "quiet" "-")
Gary is rough.
Unknown
rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "rough" "+")
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "white" "-")
Gary is young.
Unknown
rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Gary" "is" "young" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Anne is cold.[(triple2)] Anne is not blue.[(triple1)] Anne is smart.[(triple3)] Erin is smart.[(triple4)] Erin is white.[(triple5)] Erin is young.[(triple6 OR ((((triple4) -> rule5)) -> rule1) OR ((((triple5) -> rule4)) -> rule1))] Gary is blue.[(triple7)] Gary is quiet.[(triple8)] Harry is not cold.[(triple9)] Harry is quiet.[(triple10)] Harry is rough.[(triple11)] Harry is smart.[(triple12)] @1: Anne is white.[(((triple3 triple1) -> rule3))] Erin is rough.[(((triple4) -> rule5) OR ((triple5) -> rule4))] Gary is not white.[(((triple7) -> rule2))] Harry is young.[(((triple11) -> rule1))] @2: Anne is rough.[(((((triple3 triple1) -> rule3)) -> rule4))] @3: Anne is young.[(((((((triple3 triple1) -> rule3)) -> rule4)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Erin is white.
("Erin" "is" "white" "+")
triple5
Erin is young.
("Erin" "is" "young" "+")
triple6
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
Harry is not cold.
("Harry" "is" "cold" "-")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Anne is white.
("Anne" "is" "white" "+")
((triple3 triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple4) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple5) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
((triple7) -> (rule2 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple11) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple3 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((((triple3 triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3