Anne is big. Anne is nice. Anne is rough. Anne is white. Erin is not big. Erin is kind. Erin is nice. Erin is quiet. Fiona is cold. Fiona is not quiet. Fiona is not rough. Harry is cold. Harry is nice. Harry is quiet. Harry is rough. Harry is not white. Quiet, big things are not rough. If Fiona is big and Fiona is not white then Fiona is cold. Rough things are nice. All kind, white things are nice. If something is rough and cold then it is nice. If something is quiet and nice then it is kind. If something is cold then it is kind. If something is kind then it is not big.
Anne is big.
("Anne" "is" "big" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Erin is not big.
("Erin" "is" "big" "-")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
Fiona is not rough.
("Fiona" "is" "rough" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not white.
("Harry" "is" "white" "-")
Quiet, big things are not rough.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "-"))
If Fiona is big and Fiona is not white then Fiona is cold.
((("Fiona" "is" "big" "+") ("Fiona" "is" "white" "~")) -> ("Fiona" "is" "cold" "+"))
Rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All kind, white things are nice.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is rough and cold then it is nice.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is quiet and nice then it is kind.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it is not big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "-"))
Anne is rough.
True
1
proof
[(triple3)]
("Anne" "is" "rough" "+")
triple3
Fiona is rough.
False
1
inv-proof
[(triple11)]
("Fiona" "is" "rough" "+")
triple11
Harry is kind.
True
2
proof
[(((triple12) -> rule7) OR ((triple14 triple13) -> rule6) OR ((triple14 ((triple15) -> rule3)) -> rule6) OR ((triple14 ((triple15 triple12) -> rule5)) -> rule6))]
("Harry" "is" "kind" "+")
((triple12) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple14 triple13) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple14 ((triple15) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple14 ((triple15 triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Fiona is not kind.
False
2
inv-proof
[(((triple9) -> rule7))]
("Fiona" "is" "kind" "-")
((triple9) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not big.
True
3
proof
[(((((triple9) -> rule7)) -> rule8))]
("Fiona" "is" "big" "-")
((((triple9) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is not big.
("Fiona" "is" "big" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Harry is big.
False
3
inv-proof
[(((((triple12) -> rule7)) -> rule8) OR ((((triple14 triple13) -> rule6)) -> rule8) OR ((((triple14 ((triple15) -> rule3)) -> rule6)) -> rule8) OR ((((triple14 ((triple15 triple12) -> rule5)) -> rule6)) -> rule8))]
("Harry" "is" "big" "+")
((((triple12) -> (rule7 % int2))) -> (rule8 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple14 triple13) -> (rule6 % int2))) -> (rule8 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple14 ((triple15) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple14 ((triple15 triple12) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "kind" "-")
Fiona is nice.
Unknown
rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "nice" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Anne is big.[(triple1)] Anne is nice.[(triple2 OR ((triple3) -> rule3))] Anne is rough.[(triple3)] Anne is white.[(triple4)] Erin is kind.[(triple6 OR ((triple8 triple7) -> rule6))] Erin is nice.[(triple7)] Erin is not big.[(triple5 OR ((triple6) -> rule8) OR ((((triple8 triple7) -> rule6)) -> rule8))] Erin is quiet.[(triple8)] Fiona is cold.[(triple9)] Fiona is not quiet.[(triple10)] Fiona is not rough.[(triple11)] Harry is cold.[(triple12)] Harry is nice.[(triple13 OR ((triple15) -> rule3) OR ((triple15 triple12) -> rule5))] Harry is not white.[(triple16)] Harry is quiet.[(triple14)] Harry is rough.[(triple15)] @1: Fiona is kind.[(((triple9) -> rule7))] Harry is kind.[(((triple12) -> rule7) OR ((triple14 triple13) -> rule6) OR ((triple14 ((triple15) -> rule3)) -> rule6) OR ((triple14 ((triple15 triple12) -> rule5)) -> rule6))] @2: Fiona is not big.[(((((triple9) -> rule7)) -> rule8))] Harry is not big.[(((((triple12) -> rule7)) -> rule8) OR ((((triple14 triple13) -> rule6)) -> rule8) OR ((((triple14 ((triple15) -> rule3)) -> rule6)) -> rule8) OR ((((triple14 ((triple15 triple12) -> rule5)) -> rule6)) -> rule8))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((triple3) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple6
((triple8 triple7) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple7
Erin is not big.
("Erin" "is" "big" "-")
triple5
((triple6) -> (rule8 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
((((triple8 triple7) -> (rule6 % int2))) -> (rule8 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
Fiona is cold.
("Fiona" "is" "cold" "+")
triple9
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
triple10
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple11
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
triple13
((triple15) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple15 triple12) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not white.
("Harry" "is" "white" "-")
triple16
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple9) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple12) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple14 triple13) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple14 ((triple15) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple14 ((triple15 triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Fiona is not big.
("Fiona" "is" "big" "-")
((((triple9) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is not big.
("Fiona" "is" "big" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Harry is not big.
("Harry" "is" "big" "-")
((((triple12) -> (rule7 % int2))) -> (rule8 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple14 triple13) -> (rule6 % int2))) -> (rule8 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple14 ((triple15) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple14 ((triple15 triple12) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3