Bob is big. Bob is blue. Bob is nice. Charlie is big. Charlie is kind. Charlie is nice. Charlie is round. Erin is kind. Erin is nice. Fiona is big. If Fiona is blue then Fiona is nice. If something is round and blue then it is kind. All big things are nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Fiona is big.
("Fiona" "is" "big" "+")
If Fiona is blue then Fiona is nice.
((("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "nice" "+"))
If something is round and blue then it is kind.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Fiona is big.
True
1
proof
[(triple10)]
("Fiona" "is" "big" "+")
triple10
Fiona is not big.
False
1
inv-proof
[(triple10)]
("Fiona" "is" "big" "-")
triple10
Fiona is nice.
True
2
proof
[(((triple10) -> rule3))]
("Fiona" "is" "nice" "+")
((triple10) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not nice.
False
2
inv-proof
[(((triple10) -> rule3))]
("Fiona" "is" "nice" "-")
((triple10) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "kind" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "kind" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is nice.[(triple3 OR ((triple1) -> rule3))] Charlie is big.[(triple4)] Charlie is kind.[(triple5)] Charlie is nice.[(triple6 OR ((triple4) -> rule3))] Charlie is round.[(triple7)] Erin is kind.[(triple8)] Erin is nice.[(triple9)] Fiona is big.[(triple10)] @1: Fiona is nice.[(((triple10) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple1) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
((triple4) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is nice.
("Erin" "is" "nice" "+")
triple9
Fiona is big.
("Fiona" "is" "big" "+")
triple10
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple10) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1