Erin is smart. Harry is not big. Harry is round. If Erin is red then Erin is smart. All green people are red. All cold people are green. Round, green people are not smart. If Harry is smart and Harry is big then Harry is rough. If Erin is green then Erin is big. All round people are rough. Round people are cold.
Erin is smart.
("Erin" "is" "smart" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is round.
("Harry" "is" "round" "+")
If Erin is red then Erin is smart.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "smart" "+"))
All green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
All cold people are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Round, green people are not smart.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "-"))
If Harry is smart and Harry is big then Harry is rough.
((("Harry" "is" "smart" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "rough" "+"))
If Erin is green then Erin is big.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "big" "+"))
All round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Erin is smart.
True
1
proof
[(triple1)]
("Erin" "is" "smart" "+")
triple1
Harry is not round.
False
1
inv-proof
[(triple3)]
("Harry" "is" "round" "-")
triple3
Harry is rough.
True
2
proof
[(((triple3) -> rule7))]
("Harry" "is" "rough" "+")
((triple3) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple3) -> rule8))]
("Harry" "is" "cold" "-")
((triple3) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
True
3
proof
[(((((triple3) -> rule8)) -> rule3))]
("Harry" "is" "green" "+")
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not green.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule3))]
("Harry" "is" "green" "-")
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is red.
True
4
proof
[(((((((triple3) -> rule8)) -> rule3)) -> rule2))]
("Harry" "is" "red" "+")
((((((triple3) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not red.
False
4
inv-proof
[(((((((triple3) -> rule8)) -> rule3)) -> rule2))]
("Harry" "is" "red" "-")
((((((triple3) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Erin is not green.
Unknown
inv-rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is big.
Unknown
rconc
[@3: Erin is big.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule8 <- FAIL)]]
("Erin" "is" "big" "+")
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is cold.
Unknown
rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "cold" "+")
@0: Erin is smart.[(triple1)] Harry is not big.[(triple2)] Harry is round.[(triple3)] @1: Harry is cold.[(((triple3) -> rule8))] Harry is rough.[(((triple3) -> rule7))] @2: Harry is green.[(((((triple3) -> rule8)) -> rule3))] @3: Harry is not smart.[(((triple3 ((((triple3) -> rule8)) -> rule3)) -> rule4))] Harry is red.[(((((((triple3) -> rule8)) -> rule3)) -> rule2))]
Erin is smart.
("Erin" "is" "smart" "+")
triple1
Harry is not big.
("Harry" "is" "big" "-")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
((triple3) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple3) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not smart.
("Harry" "is" "smart" "-")
((triple3 ((((triple3) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((((triple3) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3