Anne is not big. Anne is blue. Anne is quiet. Anne is not red. Anne is rough. Anne is not smart. Erin is big. Erin is nice. Erin is quiet. Erin is not red. Erin is rough. Erin is smart. Harry is not blue. Harry is quiet. Harry is not rough. If someone is blue then they are rough. If someone is smart then they are blue. If someone is big then they are smart. If Erin is not red and Erin is not rough then Erin is not nice. All nice people are quiet. Blue people are quiet. All quiet, big people are nice. If someone is quiet and not big then they are nice.
Anne is not big.
("Anne" "is" "big" "-")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not red.
("Anne" "is" "red" "-")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Erin is big.
("Erin" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is not red.
("Erin" "is" "red" "-")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
If someone is blue then they are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone is smart then they are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If someone is big then they are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If Erin is not red and Erin is not rough then Erin is not nice.
((("Erin" "is" "red" "~") ("Erin" "is" "rough" "~")) -> ("Erin" "is" "nice" "-"))
All nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Blue people are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
All quiet, big people are nice.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is quiet and not big then they are nice.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "nice" "+"))
Anne is not big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Erin is not big.
False
1
inv-proof
[(triple7)]
("Erin" "is" "big" "-")
triple7
Erin is blue.
True
2
proof
[(((triple12) -> rule2) OR ((((triple7) -> rule3)) -> rule2))]
("Erin" "is" "blue" "+")
((triple12) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Anne is not nice.
False
3
inv-proof
[(((triple3 triple1) -> rule8) OR ((((triple2) -> rule6) triple1) -> rule8))]
("Anne" "is" "nice" "-")
((triple3 triple1) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple2) -> (rule6 % int2)) triple1) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "smart" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Anne is blue.[(triple2)] Anne is not big.[(triple1)] Anne is not red.[(triple4)] Anne is not smart.[(triple6)] Anne is quiet.[(triple3 OR ((triple2) -> rule6))] Anne is rough.[(triple5 OR ((triple2) -> rule1))] Erin is big.[(triple7)] Erin is nice.[(triple8 OR ((triple9 triple7) -> rule7) OR ((((((triple12) -> rule2)) -> rule6) triple7) -> rule7) OR ((((((((triple7) -> rule3)) -> rule2)) -> rule6) triple7) -> rule7))] Erin is not red.[(triple10)] Erin is quiet.[(triple9 OR ((triple8) -> rule5) OR ((((triple12) -> rule2)) -> rule6) OR ((((((triple7) -> rule3)) -> rule2)) -> rule6))] Erin is rough.[(triple11 OR ((((triple12) -> rule2)) -> rule1) OR ((((((triple7) -> rule3)) -> rule2)) -> rule1))] Erin is smart.[(triple12 OR ((triple7) -> rule3))] Harry is not blue.[(triple13)] Harry is not rough.[(triple15)] Harry is quiet.[(triple14)] @1: Anne is nice.[(((triple3 triple1) -> rule8) OR ((((triple2) -> rule6) triple1) -> rule8))] Erin is blue.[(((triple12) -> rule2) OR ((((triple7) -> rule3)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is not big.
("Anne" "is" "big" "-")
triple1
Anne is not red.
("Anne" "is" "red" "-")
triple4
Anne is not smart.
("Anne" "is" "smart" "-")
triple6
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((triple2) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
triple8
((triple9 triple7) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((((triple12) -> (rule2 % int3))) -> (rule6 % int2)) triple7) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((((triple7) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule6 % int2)) triple7) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is not red.
("Erin" "is" "red" "-")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
((triple8) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple12) -> (rule2 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((((triple7) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
triple11
((((triple12) -> (rule2 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((((triple7) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
triple12
((triple7) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
triple13
Harry is not rough.
("Harry" "is" "rough" "-")
triple15
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Anne is nice.
("Anne" "is" "nice" "+")
((triple3 triple1) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple2) -> (rule6 % int2)) triple1) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((triple12) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2