Charlie is kind. Dave is nice. Fiona is smart. Harry is cold. White things are rough. All rough things are young. All kind things are white. If Fiona is kind then Fiona is white. All young things are cold. If something is white and not young then it is nice.
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is cold.
("Harry" "is" "cold" "+")
White things are rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
All rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
All kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If Fiona is kind then Fiona is white.
((("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "white" "+"))
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is white and not young then it is nice.
((("something" "is" "white" "+") ("something" "is" "young" "~")) -> ("something" "is" "nice" "+"))
Dave is nice.
True
1
proof
[(triple2)]
("Dave" "is" "nice" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple4)]
("Harry" "is" "cold" "-")
triple4
Charlie is white.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "white" "+")
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "white" "-")
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Charlie" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not rough.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Charlie" "is" "rough" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Fiona is not rough.
Unknown
inv-rconc
[@2: Fiona is rough.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is cold.
Unknown
rconc
[@4: Fiona is cold.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "cold" "+")
Harry is not rough.
Unknown
inv-rconc
[@2: Harry is rough.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Harry" "is" "rough" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Charlie is kind.[(triple1)] Dave is nice.[(triple2)] Fiona is smart.[(triple3)] Harry is cold.[(triple4)] @1: Charlie is white.[(((triple1) -> rule3))] @2: Charlie is rough.[(((((triple1) -> rule3)) -> rule1))] @3: Charlie is young.[(((((((triple1) -> rule3)) -> rule1)) -> rule2))] @4: Charlie is cold.[(((((((((triple1) -> rule3)) -> rule1)) -> rule2)) -> rule5))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4