Bob is nice. Bob is smart. Charlie is furry. Erin is blue. Erin is green. Erin is smart. Fiona is blue. Fiona is kind. Fiona is nice. Fiona is smart. Green things are smart. Furry things are kind. If something is kind then it is nice. If Fiona is smart and Fiona is blue then Fiona is white. If Erin is kind and Erin is furry then Erin is nice. Furry, nice things are blue.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it is nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If Fiona is smart and Fiona is blue then Fiona is white.
((("Fiona" "is" "smart" "+") ("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "white" "+"))
If Erin is kind and Erin is furry then Erin is nice.
((("Erin" "is" "kind" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "nice" "+"))
Furry, nice things are blue.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Fiona is blue.
True
1
proof
[(triple7)]
("Fiona" "is" "blue" "+")
triple7
Charlie is not furry.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "furry" "-")
triple3
Fiona is white.
True
3
proof
[(((triple10 triple7) -> rule4))]
("Fiona" "is" "white" "+")
((triple10 triple7) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is not white.
False
3
inv-proof
[(((triple10 triple7) -> rule4))]
("Fiona" "is" "white" "-")
((triple10 triple7) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Charlie is nice.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Charlie" "is" "nice" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not nice.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Charlie" "is" "nice" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
True
5
proof
[(((triple3 ((((triple3) -> rule2)) -> rule3)) -> rule6))]
("Charlie" "is" "blue" "+")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not blue.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule2)) -> rule3)) -> rule6))]
("Charlie" "is" "blue" "-")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "blue" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "smart" "+")
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "kind" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "kind" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is nice.[(triple1)] Bob is smart.[(triple2)] Charlie is furry.[(triple3)] Erin is blue.[(triple4)] Erin is green.[(triple5)] Erin is smart.[(triple6 OR ((triple5) -> rule1))] Fiona is blue.[(triple7)] Fiona is kind.[(triple8)] Fiona is nice.[(triple9 OR ((triple8) -> rule3))] Fiona is smart.[(triple10)] @1: Charlie is kind.[(((triple3) -> rule2))] Fiona is white.[(((triple10 triple7) -> rule4))] @2: Charlie is nice.[(((((triple3) -> rule2)) -> rule3))] @3: Charlie is blue.[(((triple3 ((((triple3) -> rule2)) -> rule3)) -> rule6))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
((triple5) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
Fiona is kind.
("Fiona" "is" "kind" "+")
triple8
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
((triple8) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple10 triple7) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3