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