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