Dave is kind. Dave is quiet. Erin is kind. Fiona is big. Fiona is kind. Fiona is nice. Fiona is quiet. Harry is big. Harry is quiet. Harry is white. If someone is white then they are quiet. All big people are kind. All nice people are white. If someone is white then they are nice. All nice people are white. If someone is quiet then they are kind.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is white then they are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
All big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
All nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If someone is white then they are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
All nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If someone is quiet then they are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Harry is big.
True
1
proof
[(triple8)]
("Harry" "is" "big" "+")
triple8
Erin is not kind.
False
1
inv-proof
[(triple3)]
("Erin" "is" "kind" "-")
triple3
Harry is kind.
True
2
proof
[(((triple8) -> rule2) OR ((triple9) -> rule6) OR ((((triple10) -> rule1)) -> rule6))]
("Harry" "is" "kind" "+")
((triple8) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple9) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Fiona is not white.
False
2
inv-proof
[(((triple6) -> rule3) OR ((triple6) -> rule5))]
("Fiona" "is" "white" "-")
((triple6) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple6) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Erin is not white.
Unknown
inv-rconc
[@3: Erin is white.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule5 <- FAIL)]]
("Erin" "is" "white" "-")
Dave is white.
Unknown
rconc
[@3: Dave is white.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule5 <- FAIL)]]
("Dave" "is" "white" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Dave is kind.[(triple1 OR ((triple2) -> rule6))] Dave is quiet.[(triple2)] Erin is kind.[(triple3)] Fiona is big.[(triple4)] Fiona is kind.[(triple5 OR ((triple4) -> rule2) OR ((triple7) -> rule6) OR ((((((triple6) -> rule3)) -> rule1)) -> rule6) OR ((((((triple6) -> rule5)) -> rule1)) -> rule6))] Fiona is nice.[(triple6)] Fiona is quiet.[(triple7 OR ((((triple6) -> rule3)) -> rule1) OR ((((triple6) -> rule5)) -> rule1))] Harry is big.[(triple8)] Harry is quiet.[(triple9 OR ((triple10) -> rule1))] Harry is white.[(triple10)] @1: Fiona is white.[(((triple6) -> rule3) OR ((triple6) -> rule5))] Harry is kind.[(((triple8) -> rule2) OR ((triple9) -> rule6) OR ((((triple10) -> rule1)) -> rule6))] Harry is nice.[(((triple10) -> rule4))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
((triple2) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
Fiona is kind.
("Fiona" "is" "kind" "+")
triple5
((triple4) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((triple7) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
((((((triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((triple6) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
((triple10) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple10
Fiona is white.
("Fiona" "is" "white" "+")
((triple6) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple6) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple8) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple9) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((triple10) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1