Bob is cold. Bob is green. Bob is kind. Bob is nice. Bob is red. Charlie is green. Charlie is nice. Charlie is smart. Fiona is green. Fiona is kind. Fiona is nice. Fiona is smart. Smart things are green. If Fiona is quiet then Fiona is red.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If Fiona is quiet then Fiona is red.
((("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "red" "+"))
Fiona is green.
True
1
proof
[(triple9 OR ((triple12) -> rule1))]
("Fiona" "is" "green" "+")
triple9
((triple12) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Bob is not red.
False
1
inv-proof
[(triple5)]
("Bob" "is" "red" "-")
triple5
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "red" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is cold.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3)] Bob is nice.[(triple4)] Bob is red.[(triple5)] Charlie is green.[(triple6 OR ((triple8) -> rule1))] Charlie is nice.[(triple7)] Charlie is smart.[(triple8)] Fiona is green.[(triple9 OR ((triple12) -> rule1))] Fiona is kind.[(triple10)] Fiona is nice.[(triple11)] Fiona is smart.[(triple12)]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
((triple8) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
Fiona is green.
("Fiona" "is" "green" "+")
triple9
((triple12) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple10
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12