Bob is kind. Bob is round. Bob is smart. Charlie is kind. Charlie is red. Charlie is smart. Fiona is red. Fiona is white. Harry is kind. Harry is smart. If something is green then it is white. All red, white things are green. White, red things are green. If something is white and round then it is kind. If Fiona is green then Fiona is smart. If Bob is red then Bob is kind.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is green then it is white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
All red, white things are green.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
White, red things are green.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is white and round then it is kind.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If Fiona is green then Fiona is smart.
((("Fiona" "is" "green" "+")) -> ("Fiona" "is" "smart" "+"))
If Bob is red then Bob is kind.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "kind" "+"))
Bob is kind.
True
1
proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Charlie is not smart.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "smart" "-")
triple6
Fiona is green.
True
3
proof
[(((triple7 triple8) -> rule2) OR ((triple8 triple7) -> rule3))]
("Fiona" "is" "green" "+")
((triple7 triple8) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple8 triple7) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is not green.
False
3
inv-proof
[(((triple7 triple8) -> rule2) OR ((triple8 triple7) -> rule3))]
("Fiona" "is" "green" "-")
((triple7 triple8) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple8 triple7) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
True
4
proof
[(((((triple7 triple8) -> rule2)) -> rule5) OR ((((triple8 triple7) -> rule3)) -> rule5))]
("Fiona" "is" "smart" "+")
((((triple7 triple8) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((((triple8 triple7) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is not smart.
False
4
inv-proof
[(((((triple7 triple8) -> rule2)) -> rule5) OR ((((triple8 triple7) -> rule3)) -> rule5))]
("Fiona" "is" "smart" "-")
((((triple7 triple8) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((((triple8 triple7) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Bob is not white.
Unknown
inv-rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Bob" "is" "white" "-")
Charlie is white.
Unknown
rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "white" "+")
Harry is not white.
Unknown
inv-rconc
[@2: Harry is white.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "white" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Bob is kind.[(triple1)] Bob is round.[(triple2)] Bob is smart.[(triple3)] Charlie is kind.[(triple4)] Charlie is red.[(triple5)] Charlie is smart.[(triple6)] Fiona is red.[(triple7)] Fiona is white.[(triple8)] Harry is kind.[(triple9)] Harry is smart.[(triple10)] @1: Fiona is green.[(((triple7 triple8) -> rule2) OR ((triple8 triple7) -> rule3))] @2: Fiona is smart.[(((((triple7 triple8) -> rule2)) -> rule5) OR ((((triple8 triple7) -> rule3)) -> rule5))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple7
Fiona is white.
("Fiona" "is" "white" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Fiona is green.
("Fiona" "is" "green" "+")
((triple7 triple8) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple8 triple7) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple7 triple8) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((((triple8 triple7) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2