Bob is quiet. Bob is red. Charlie is not cold. Charlie is kind. Charlie is red. Fiona is cold. Fiona is kind. Fiona is red. Gary is cold. Gary is quiet. Gary is red. Gary is not white. All quiet, young things are not cold. If something is white then it is young. White things are young. Red things are kind. If something is kind and not white then it is not smart. If something is red and not cold then it is smart.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is not white.
("Gary" "is" "white" "-")
All quiet, young things are not cold.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "-"))
If something is white then it is young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
White things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
Red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is kind and not white then it is not smart.
((("something" "is" "kind" "+") ("something" "is" "white" "~")) -> ("something" "is" "smart" "-"))
If something is red and not cold then it is smart.
((("something" "is" "red" "+") ("something" "is" "cold" "~")) -> ("something" "is" "smart" "+"))
Fiona is red.
True
1
proof
[(triple8)]
("Fiona" "is" "red" "+")
triple8
Bob is not quiet.
False
1
inv-proof
[(triple1)]
("Bob" "is" "quiet" "-")
triple1
Gary is kind.
True
2
proof
[(((triple11) -> rule4))]
("Gary" "is" "kind" "+")
((triple11) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple2) -> rule4))]
("Bob" "is" "kind" "-")
((triple2) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Gary is not smart.
True
4
proof
[(((((triple11) -> rule4) triple12) -> rule5))]
("Gary" "is" "smart" "-")
((((triple11) -> (rule4 % int2)) triple12) -> (rule5 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is smart.
False
4
inv-proof
[(((((triple11) -> rule4) triple12) -> rule5))]
("Gary" "is" "smart" "+")
((((triple11) -> (rule4 % int2)) triple12) -> (rule5 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "young" "-")
Fiona is smart.
Unknown
rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "smart" "+")
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "smart" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Bob is quiet.[(triple1)] Bob is red.[(triple2)] Charlie is kind.[(triple4 OR ((triple5) -> rule4))] Charlie is not cold.[(triple3)] Charlie is red.[(triple5)] Fiona is cold.[(triple6)] Fiona is kind.[(triple7 OR ((triple8) -> rule4))] Fiona is red.[(triple8)] Gary is cold.[(triple9)] Gary is not white.[(triple12)] Gary is quiet.[(triple10)] Gary is red.[(triple11)] @1: Bob is kind.[(((triple2) -> rule4))] Charlie is smart.[(((triple5 triple3) -> rule6))] Gary is kind.[(((triple11) -> rule4))] @2: Gary is not smart.[(((((triple11) -> rule4) triple12) -> rule5))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
((triple5) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Fiona is kind.
("Fiona" "is" "kind" "+")
triple7
((triple8) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is not white.
("Gary" "is" "white" "-")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple5 triple3) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple11) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not smart.
("Gary" "is" "smart" "-")
((((triple11) -> (rule4 % int2)) triple12) -> (rule5 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2