Anne is round. Erin is smart. Fiona is not big. Harry is smart. Big people are kind. All blue, big people are not kind. If someone is smart then they are rough. Big people are nice. Smart, big people are blue. If someone is rough then they are not blue. Round people are smart. If Anne is kind and Anne is smart then Anne is rough.
Anne is round.
("Anne" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
Harry is smart.
("Harry" "is" "smart" "+")
Big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
All blue, big people are not kind.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "-"))
If someone is smart then they are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Smart, big people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough then they are not blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "-"))
Round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If Anne is kind and Anne is smart then Anne is rough.
((("Anne" "is" "kind" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "rough" "+"))
Fiona is not big.
True
1
proof
[(triple3)]
("Fiona" "is" "big" "-")
triple3
Fiona is big.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "big" "+")
triple3
Erin is rough.
True
2
proof
[(((triple2) -> rule3))]
("Erin" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule7))]
("Anne" "is" "smart" "-")
((triple1) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Harry is not blue.
True
3
proof
[(((((triple4) -> rule3)) -> rule6))]
("Harry" "is" "blue" "-")
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Anne is not rough.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule3))]
("Anne" "is" "rough" "-")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "smart" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "kind" "+")
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "nice" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is round.[(triple1)] Erin is smart.[(triple2)] Fiona is not big.[(triple3)] Harry is smart.[(triple4)] @1: Anne is smart.[(((triple1) -> rule7))] Erin is rough.[(((triple2) -> rule3))] Harry is rough.[(((triple4) -> rule3))] @2: Anne is rough.[(((((triple1) -> rule7)) -> rule3))] Erin is not blue.[(((((triple2) -> rule3)) -> rule6))] Harry is not blue.[(((((triple4) -> rule3)) -> rule6))] @3: Anne is not blue.[(((((((triple1) -> rule7)) -> rule3)) -> rule6))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Fiona is not big.
("Fiona" "is" "big" "-")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Harry is not blue.
("Harry" "is" "blue" "-")
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Anne is not blue.
("Anne" "is" "blue" "-")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3