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