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