Bob is kind. Bob is round. Bob is young. Charlie is cold. Dave is cold. Dave is red. Fiona is not kind. Quiet things are round. If Dave is cold and Dave is young then Dave is round. Round things are kind. If something is cold then it is kind. If something is smart and kind then it is red. Kind things are cold.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is not kind.
("Fiona" "is" "kind" "-")
Quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If Dave is cold and Dave is young then Dave is round.
((("Dave" "is" "cold" "+") ("Dave" "is" "young" "+")) -> ("Dave" "is" "round" "+"))
Round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is smart and kind then it is red.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
Dave is red.
True
1
proof
[(triple6)]
("Dave" "is" "red" "+")
triple6
Dave is not cold.
False
1
inv-proof
[(triple5)]
("Dave" "is" "cold" "-")
triple5
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Bob is kind.[(triple1 OR ((triple2) -> rule3))] Bob is round.[(triple2)] Bob is young.[(triple3)] Charlie is cold.[(triple4)] Dave is cold.[(triple5)] Dave is red.[(triple6)] Fiona is not kind.[(triple7)] @1: Bob is cold.[(((triple1) -> rule6) OR ((((triple2) -> rule3)) -> rule6))] Charlie is kind.[(((triple4) -> rule4))] Dave is kind.[(((triple5) -> rule4))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple4) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple5) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1