Erin is kind. Erin is round. Harry is quiet. All big, cold things are quiet. All big, round things are not quiet. If something is quiet then it is not rough. If Erin is round then Erin is kind. If something is quiet then it is blue. All round things are cold. All blue things are not round. If Harry is blue then Harry is quiet.
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All big, cold things are quiet.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All big, round things are not quiet.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "-"))
If something is quiet then it is not rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "-"))
If Erin is round then Erin is kind.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "kind" "+"))
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
All round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
All blue things are not round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "-"))
If Harry is blue then Harry is quiet.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "quiet" "+"))
Erin is kind.
True
1
proof
[(triple1 OR ((triple2) -> rule4))]
("Erin" "is" "kind" "+")
triple1
((triple2) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Harry is not quiet.
False
1
inv-proof
[(triple3)]
("Harry" "is" "quiet" "-")
triple3
Harry is blue.
True
2
proof
[(((triple3) -> rule5))]
("Harry" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple2) -> rule6))]
("Erin" "is" "cold" "-")
((triple2) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Harry is not round.
True
3
proof
[(((((triple3) -> rule5)) -> rule7))]
("Harry" "is" "round" "-")
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule7))]
("Harry" "is" "round" "+")
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is blue.
Unknown
rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Erin" "is" "blue" "+")
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "cold" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Erin is kind.[(triple1 OR ((triple2) -> rule4))] Erin is round.[(triple2)] Harry is quiet.[(triple3)] @1: Erin is cold.[(((triple2) -> rule6))] Harry is blue.[(((triple3) -> rule5))] Harry is not rough.[(((triple3) -> rule3))] @2: Harry is not round.[(((((triple3) -> rule5)) -> rule7))]
Erin is kind.
("Erin" "is" "kind" "+")
triple1
((triple2) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
((triple2) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not rough.
("Harry" "is" "rough" "-")
((triple3) -> (rule3 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is not round.
("Harry" "is" "round" "-")
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2