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