Charlie is nice. Charlie is not quiet. Charlie is young. Fiona is big. Fiona is not nice. Fiona is not red. Fiona is not smart. Fiona is not white. Gary is nice. Gary is white. Gary is young. Harry is nice. Quiet, smart things are young. All smart, quiet things are nice. If something is big then it is not nice. If something is smart and red then it is not quiet. If something is big and red then it is white. All red things are smart. All nice things are red. If something is smart and quiet then it is not big.
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is not nice.
("Fiona" "is" "nice" "-")
Fiona is not red.
("Fiona" "is" "red" "-")
Fiona is not smart.
("Fiona" "is" "smart" "-")
Fiona is not white.
("Fiona" "is" "white" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Quiet, smart things are young.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
All smart, quiet things are nice.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
If something is big then it is not nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "-"))
If something is smart and red then it is not quiet.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "-"))
If something is big and red then it is white.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
All red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
All nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something is smart and quiet then it is not big.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "-"))
Fiona is not nice.
True
1
proof
[(triple5 OR ((triple4) -> rule3))]
("Fiona" "is" "nice" "-")
triple5
((triple4) -> (rule3 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is nice.
False
1
inv-proof
[(triple5 OR ((triple4) -> rule3))]
("Fiona" "is" "nice" "+")
triple5
((triple4) -> (rule3 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Charlie is red.
True
2
proof
[(((triple1) -> rule7))]
("Charlie" "is" "red" "+")
((triple1) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple1) -> rule7))]
("Charlie" "is" "red" "-")
((triple1) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Harry is smart.
True
3
proof
[(((((triple12) -> rule7)) -> rule6))]
("Harry" "is" "smart" "+")
((((triple12) -> (rule7 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((((triple9) -> rule7)) -> rule6))]
("Gary" "is" "smart" "-")
((((triple9) -> (rule7 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "young" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "white" "+")
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "white" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Charlie is nice.[(triple1)] Charlie is not quiet.[(triple2 OR ((((((triple1) -> rule7)) -> rule6) ((triple1) -> rule7)) -> rule4))] Charlie is young.[(triple3)] Fiona is big.[(triple4)] Fiona is not nice.[(triple5 OR ((triple4) -> rule3))] Fiona is not red.[(triple6)] Fiona is not smart.[(triple7)] Fiona is not white.[(triple8)] Gary is nice.[(triple9)] Gary is white.[(triple10)] Gary is young.[(triple11)] Harry is nice.[(triple12)] @1: Charlie is red.[(((triple1) -> rule7))] Gary is red.[(((triple9) -> rule7))] Harry is red.[(((triple12) -> rule7))] @2: Charlie is smart.[(((((triple1) -> rule7)) -> rule6))] Gary is smart.[(((((triple9) -> rule7)) -> rule6))] Harry is smart.[(((((triple12) -> rule7)) -> rule6))] @3: Gary is not quiet.[(((((((triple9) -> rule7)) -> rule6) ((triple9) -> rule7)) -> rule4))] Harry is not quiet.[(((((((triple12) -> rule7)) -> rule6) ((triple12) -> rule7)) -> rule4))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple2
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2)) ((triple1) -> (rule7 % int3))) -> (rule4 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
Fiona is not nice.
("Fiona" "is" "nice" "-")
triple5
((triple4) -> (rule3 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is not red.
("Fiona" "is" "red" "-")
triple6
Fiona is not smart.
("Fiona" "is" "smart" "-")
triple7
Fiona is not white.
("Fiona" "is" "white" "-")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Gary is young.
("Gary" "is" "young" "+")
triple11
Harry is nice.
("Harry" "is" "nice" "+")
triple12
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple9) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple12) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple9) -> (rule7 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple12) -> (rule7 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Gary is not quiet.
("Gary" "is" "quiet" "-")
((((((triple9) -> (rule7 % int3))) -> (rule6 % int2)) ((triple9) -> (rule7 % int3))) -> (rule4 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Harry is not quiet.
("Harry" "is" "quiet" "-")
((((((triple12) -> (rule7 % int3))) -> (rule6 % int2)) ((triple12) -> (rule7 % int3))) -> (rule4 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3