Anne is red. Bob is blue. Bob is kind. Bob is nice. Bob is round. Erin is not blue. Erin is kind. Erin is red. Erin is not round. Erin is not white. Harry is not nice. Harry is round. If Erin is blue and Erin is red then Erin is not kind. If Harry is nice then Harry is not round. All blue things are green. Nice things are red. If something is green then it is red. All green, red things are nice. If something is round and not nice then it is kind. If Harry is round and Harry is kind then Harry is white.
Anne is red.
("Anne" "is" "red" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is not round.
("Erin" "is" "round" "-")
Erin is not white.
("Erin" "is" "white" "-")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is round.
("Harry" "is" "round" "+")
If Erin is blue and Erin is red then Erin is not kind.
((("Erin" "is" "blue" "+") ("Erin" "is" "red" "+")) -> ("Erin" "is" "kind" "-"))
If Harry is nice then Harry is not round.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "round" "-"))
All blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something is green then it is red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All green, red things are nice.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something is round and not nice then it is kind.
((("something" "is" "round" "+") ("something" "is" "nice" "~")) -> ("something" "is" "kind" "+"))
If Harry is round and Harry is kind then Harry is white.
((("Harry" "is" "round" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "white" "+"))
Bob is round.
True
1
proof
[(triple5)]
("Bob" "is" "round" "+")
triple5
Bob is not nice.
False
1
inv-proof
[(triple4 OR ((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule5)) -> rule6))]
("Bob" "is" "nice" "-")
triple4
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is red.[(triple1)] Bob is blue.[(triple2)] Bob is kind.[(triple3)] Bob is nice.[(triple4 OR ((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule5)) -> rule6))] Bob is round.[(triple5)] Erin is kind.[(triple7)] Erin is not blue.[(triple6)] Erin is not round.[(triple9)] Erin is not white.[(triple10)] Erin is red.[(triple8)] Harry is not nice.[(triple11)] Harry is round.[(triple12)] @1: Bob is green.[(((triple2) -> rule3))] Bob is red.[(((triple4) -> rule4) OR ((((triple2) -> rule3)) -> rule5))] Harry is kind.[(((triple12 triple11) -> rule7))] @2: Harry is white.[(((triple12 ((triple12 triple11) -> rule7)) -> rule8))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is not blue.
("Erin" "is" "blue" "-")
triple6
Erin is not round.
("Erin" "is" "round" "-")
triple9
Erin is not white.
("Erin" "is" "white" "-")
triple10
Erin is red.
("Erin" "is" "red" "+")
triple8
Harry is not nice.
("Harry" "is" "nice" "-")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple4) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((triple12 triple11) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple12 ((triple12 triple11) -> (rule7 % int2))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2