Bob is red. Erin is red. Fiona is smart. Red people are big. All furry people are kind. If someone is red and quiet then they are kind.
Bob is red.
("Bob" "is" "red" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
All furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If someone is red and quiet then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Erin is red.
True
1
proof
[(triple2)]
("Erin" "is" "red" "+")
triple2
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Bob is big.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "big" "+")
((triple1) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple2) -> rule1))]
("Erin" "is" "big" "-")
((triple2) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "kind" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is red.[(triple1)] Erin is red.[(triple2)] Fiona is smart.[(triple3)] @1: Bob is big.[(((triple1) -> rule1))] Erin is big.[(((triple2) -> rule1))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple2) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1